Metamath Proof Explorer

Theorem mainer

Description: The Main Theorem of Equivalences: every equivalence relation implies equivalent comembers. (Contributed by Peter Mazsa, 26-Sep-2021)

Ref Expression
Assertion mainer 
|- ( R ErALTV A -> CoMembEr A )

Proof

Step Hyp Ref Expression
1 eqvrelqseqdisj2 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ElDisj A )
2 eldisjim 
 |-  ( ElDisj A -> CoElEqvRel A )
3 1 2 syl 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> CoElEqvRel A )
4 n0eldmqseq 
 |-  ( ( dom R /. R ) = A -> -. (/) e. A )
5 4 adantl 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> -. (/) e. A )
6 eldisjn0el 
 |-  ( ElDisj A -> ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) )
7 1 6 syl 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) )
8 5 7 mpbid 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ( U. A /. ~ A ) = A )
9 3 8 jca 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )
10 dferALTV2 
 |-  ( R ErALTV A <-> ( EqvRel R /\ ( dom R /. R ) = A ) )
11 dfcomember3 
 |-  ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )
12 9 10 11 3imtr4i 
 |-  ( R ErALTV A -> CoMembEr A )