Metamath Proof Explorer

Theorem erim2

Description: Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 in a more convenient form , see also erim ). (Contributed by Rodolfo Medina, 19-Oct-2010) (Proof shortened by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 29-Dec-2021)

Ref Expression
Assertion erim2 
|- ( R e. V -> ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ~ A = R ) )

Proof

Step Hyp Ref Expression
1 relcoels 
 |-  Rel ~ A
2 1 a1i 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> Rel ~ A )
3 eqvrelrel 
 |-  ( EqvRel R -> Rel R )
4 3 ad2antrl 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> Rel R )
5 brcoels 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x ~ A y <-> E. u e. A ( x e. u /\ y e. u ) ) )
6 5 el2v 
 |-  ( x ~ A y <-> E. u e. A ( x e. u /\ y e. u ) )
7 simpll 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> EqvRel R )
8 simprl 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> u e. A )
9 simplr 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> ( dom R /. R ) = A )
10 8 9 eleqtrrd 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> u e. ( dom R /. R ) )
11 simprr 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> x e. u )
12 eqvrelqsel 
 |-  ( ( EqvRel R /\ u e. ( dom R /. R ) /\ x e. u ) -> u = [ x ] R )
13 7 10 11 12 syl3anc 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> u = [ x ] R )
14 13 eleq2d 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> ( y e. u <-> y e. [ x ] R ) )
15 elecALTV 
 |-  ( ( x e. _V /\ y e. _V ) -> ( y e. [ x ] R <-> x R y ) )
16 15 el2v 
 |-  ( y e. [ x ] R <-> x R y )
17 14 16 bitrdi 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ ( u e. A /\ x e. u ) ) -> ( y e. u <-> x R y ) )
18 17 anassrs 
 |-  ( ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ u e. A ) /\ x e. u ) -> ( y e. u <-> x R y ) )
19 18 pm5.32da 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ u e. A ) -> ( ( x e. u /\ y e. u ) <-> ( x e. u /\ x R y ) ) )
20 19 rexbidva 
 |-  ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ( E. u e. A ( x e. u /\ y e. u ) <-> E. u e. A ( x e. u /\ x R y ) ) )
21 20 adantl 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( E. u e. A ( x e. u /\ y e. u ) <-> E. u e. A ( x e. u /\ x R y ) ) )
22 simpll 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ x R y ) -> EqvRel R )
23 simpr 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ x R y ) -> x R y )
24 22 23 eqvrelcl 
 |-  ( ( ( EqvRel R /\ ( dom R /. R ) = A ) /\ x R y ) -> x e. dom R )
25 24 adantll 
 |-  ( ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) /\ x R y ) -> x e. dom R )
26 eqvrelim 
 |-  ( EqvRel R -> dom R = ran R )
27 26 ad2antrl 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> dom R = ran R )
28 27 eleq2d 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x e. dom R <-> x e. ran R ) )
29 dmqseqim2 
 |-  ( R e. V -> ( Rel R -> ( ( dom R /. R ) = A -> ( x e. ran R <-> x e. U. A ) ) ) )
30 3 29 syl5 
 |-  ( R e. V -> ( EqvRel R -> ( ( dom R /. R ) = A -> ( x e. ran R <-> x e. U. A ) ) ) )
31 30 imp32 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x e. ran R <-> x e. U. A ) )
32 28 31 bitrd 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x e. dom R <-> x e. U. A ) )
33 eluni2 
 |-  ( x e. U. A <-> E. u e. A x e. u )
34 32 33 bitrdi 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x e. dom R <-> E. u e. A x e. u ) )
35 34 adantr 
 |-  ( ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) /\ x R y ) -> ( x e. dom R <-> E. u e. A x e. u ) )
36 25 35 mpbid 
 |-  ( ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) /\ x R y ) -> E. u e. A x e. u )
37 36 ex 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x R y -> E. u e. A x e. u ) )
38 37 pm4.71rd 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x R y <-> ( E. u e. A x e. u /\ x R y ) ) )
39 r19.41v 
 |-  ( E. u e. A ( x e. u /\ x R y ) <-> ( E. u e. A x e. u /\ x R y ) )
40 38 39 bitr4di 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x R y <-> E. u e. A ( x e. u /\ x R y ) ) )
41 21 40 bitr4d 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( E. u e. A ( x e. u /\ y e. u ) <-> x R y ) )
42 6 41 syl5bb 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ( x ~ A y <-> x R y ) )
43 2 4 42 eqbrrdv 
 |-  ( ( R e. V /\ ( EqvRel R /\ ( dom R /. R ) = A ) ) -> ~ A = R )
44 43 ex 
 |-  ( R e. V -> ( ( EqvRel R /\ ( dom R /. R ) = A ) -> ~ A = R ) )