Metamath Proof Explorer

Theorem ener

Description: Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998) (Revised by Mario Carneiro, 15-Nov-2014) (Proof shortened by AV, 1-May-2021)

Ref Expression
Assertion ener 
|- ~~ Er _V

Proof

Step Hyp Ref Expression
1 relen 
 |-  Rel ~~
2 bren 
 |-  ( x ~~ y <-> E. f f : x -1-1-onto-> y )
3 vex 
 |-  y e. _V
4 vex 
 |-  x e. _V
5 f1ocnv 
 |-  ( f : x -1-1-onto-> y -> `' f : y -1-1-onto-> x )
6 f1oen2g 
 |-  ( ( y e. _V /\ x e. _V /\ `' f : y -1-1-onto-> x ) -> y ~~ x )
7 3 4 5 6 mp3an12i 
 |-  ( f : x -1-1-onto-> y -> y ~~ x )
8 7 exlimiv 
 |-  ( E. f f : x -1-1-onto-> y -> y ~~ x )
9 2 8 sylbi 
 |-  ( x ~~ y -> y ~~ x )
10 bren 
 |-  ( x ~~ y <-> E. g g : x -1-1-onto-> y )
11 bren 
 |-  ( y ~~ z <-> E. f f : y -1-1-onto-> z )
12 exdistrv 
 |-  ( E. g E. f ( g : x -1-1-onto-> y /\ f : y -1-1-onto-> z ) <-> ( E. g g : x -1-1-onto-> y /\ E. f f : y -1-1-onto-> z ) )
13 vex 
 |-  z e. _V
14 f1oco 
 |-  ( ( f : y -1-1-onto-> z /\ g : x -1-1-onto-> y ) -> ( f o. g ) : x -1-1-onto-> z )
15 14 ancoms 
 |-  ( ( g : x -1-1-onto-> y /\ f : y -1-1-onto-> z ) -> ( f o. g ) : x -1-1-onto-> z )
16 f1oen2g 
 |-  ( ( x e. _V /\ z e. _V /\ ( f o. g ) : x -1-1-onto-> z ) -> x ~~ z )
17 4 13 15 16 mp3an12i 
 |-  ( ( g : x -1-1-onto-> y /\ f : y -1-1-onto-> z ) -> x ~~ z )
18 17 exlimivv 
 |-  ( E. g E. f ( g : x -1-1-onto-> y /\ f : y -1-1-onto-> z ) -> x ~~ z )
19 12 18 sylbir 
 |-  ( ( E. g g : x -1-1-onto-> y /\ E. f f : y -1-1-onto-> z ) -> x ~~ z )
20 10 11 19 syl2anb 
 |-  ( ( x ~~ y /\ y ~~ z ) -> x ~~ z )
21 4 enref 
 |-  x ~~ x
22 4 21 2th 
 |-  ( x e. _V <-> x ~~ x )
23 1 9 20 22 iseri 
 |-  ~~ Er _V