After my PR https://github.com/metamath/set.mm/pull/4531/files ,
someone added the 555669 line to set.mm:
555668 Peter Mazsa, 16-Jun-2024.)
555669 [dferALTV2 on { A } + pet imply ( dom |` { A } ) /. |` { A } )
) = { A } ]
555670 $)
555671 trressn $p |-
i.e. that
dferALTV2 $p |- ( ,~ ( R |X. ( `' _E |` { A } ) ) ErALTV { A } <-> (
EqvRel ,~ ( R |X. ( `' _E |` { A } ) ) /\ ( dom ,~ ( R |X. ( `' _E |`
{ A } ) ) /. ,~ ( R |X. ( `' _E |` { A } ) ) ) = { A } ) ) and
pet $p |- ( ( R |X. ( `' _E |` { A } ) ) Part { A } <-> ,~ ( R |X. (
`' _E |` { A } ) ) ErALTV { A } )
(and perhaps
eqvrel1cossressn $p |- ( A e. V -> EqvRel ,~ ( R |X. ( `' _E |` { A } ) ) ) and
disjressn $p |- Disj ( R |X. ( `' _E |` { A } ) ) )
would somehow imply
( dom ( R |X. ( `' _E |` { A } ) ) /. ( R |X. ( `' _E |` { A } ) ) ) = { A } .
I would be happy if this were true: does the person who added 555669
remember the train of thought?
P.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/CAJJTU5oS%2BSEKE71-BX-nhUpcdKVMbohANX1gHMCmcT%3D3eWBf9Q%40mail.gmail.com.
