Theorem mpets

Description: Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet , the Partition-Equivalence Theorem, with general R . (Contributed by Peter Mazsa, 31-Dec-2024)

	Ref	Expression
Assertion	mpets	Could not format assertion : No typesetting found for |- MembParts = CoMembErs with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mpets2	Could not format ( a e. _V -> ( ( `' _E |` a ) Parts a <-> ,~ ( `' _E |` a ) Ers a ) ) : No typesetting found for |- ( a e. _V -> ( ( `' _E |` a ) Parts a <-> ,~ ( `' _E |` a ) Ers a ) ) with typecode |-
2	1	elv	Could not format ( ( `' _E |` a ) Parts a <-> ,~ ( `' _E |` a ) Ers a ) : No typesetting found for |- ( ( `' _E |` a ) Parts a <-> ,~ ( `' _E |` a ) Ers a ) with typecode |-
3	2	abbii	Could not format { a | ( `' _E |` a ) Parts a } = { a | ,~ ( `' _E |` a ) Ers a } : No typesetting found for |- { a | ( `' _E |` a ) Parts a } = { a | ,~ ( `' _E |` a ) Ers a } with typecode |-
4		df-membparts	Could not format MembParts = { a | ( `' _E |` a ) Parts a } : No typesetting found for |- MembParts = { a | ( `' _E |` a ) Parts a } with typecode |-
5		df-comembers	Could not format CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } : No typesetting found for |- CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } with typecode |-
6	3 4 5	3eqtr4i	Could not format MembParts = CoMembErs : No typesetting found for |- MembParts = CoMembErs with typecode |-