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

Metamath Proof Explorer

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