Theorem cpet2

Description: The conventional form of the Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have called disjoint or partition what we call element disjoint or member partition, see also cpet . Together with cpet , mpet mpet2 , this is what we used to think of as the partition equivalence theorem (but cf. pet2 with general R ). (Contributed by Peter Mazsa, 30-Dec-2024)

	Ref	Expression
Assertion	cpet2	|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( EqvRel ~ 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		eqvreldmqs2	|- ( ( EqvRel ,~ ( `' _E |` A ) /\ ( dom ,~ ( `' _E |` A ) /. ,~ ( `' _E |` A ) ) = A ) <-> ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) )
5	1 3 4	3bitri	|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) )