Theorem mpet3

Description: Member Partition-Equivalence Theorem. Together with mpet mpet2 , mostly in its conventional cpet and cpet2 form, this is what we used to think of as the partition equivalence theorem (but cf. pet2 with general R ). (Contributed by Peter Mazsa, 4-May-2018) (Revised by Peter Mazsa, 26-Sep-2021)

	Ref	Expression
Assertion	mpet3	|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		eldisjn0elb	|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( Disj ( `' _E |` A ) /\ ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) )
2		eqvrelqseqdisj3	|- ( ( EqvRel ,~ ( `' _E |` A ) /\ ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) -> Disj ( `' _E |` A ) )
3	2	petlem	|- ( ( Disj ( `' _E |` A ) /\ ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) <-> ( EqvRel ,~ ( `' _E |` A ) /\ ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) )
4		eqvreldmqs	|- ( ( EqvRel ,~ ( `' _E |` A ) /\ ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )
5	1 3 4	3bitri	|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )