This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )