Metamath Proof Explorer

Theorem r111

Description: The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013)

Ref Expression
Assertion r111 
|- R1 : On -1-1-> _V

Proof

Step Hyp Ref Expression
1 r1fnon 
 |-  R1 Fn On
2 dffn2 
 |-  ( R1 Fn On <-> R1 : On --> _V )
3 1 2 mpbi 
 |-  R1 : On --> _V
4 eloni 
 |-  ( x e. On -> Ord x )
5 eloni 
 |-  ( y e. On -> Ord y )
6 ordtri3or 
 |-  ( ( Ord x /\ Ord y ) -> ( x e. y \/ x = y \/ y e. x ) )
7 4 5 6 syl2an 
 |-  ( ( x e. On /\ y e. On ) -> ( x e. y \/ x = y \/ y e. x ) )
8 sdomirr 
 |-  -. ( R1 ` y ) ~< ( R1 ` y )
9 r1sdom 
 |-  ( ( y e. On /\ x e. y ) -> ( R1 ` x ) ~< ( R1 ` y ) )
10 breq1 
 |-  ( ( R1 ` x ) = ( R1 ` y ) -> ( ( R1 ` x ) ~< ( R1 ` y ) <-> ( R1 ` y ) ~< ( R1 ` y ) ) )
11 9 10 syl5ibcom 
 |-  ( ( y e. On /\ x e. y ) -> ( ( R1 ` x ) = ( R1 ` y ) -> ( R1 ` y ) ~< ( R1 ` y ) ) )
12 8 11 mtoi 
 |-  ( ( y e. On /\ x e. y ) -> -. ( R1 ` x ) = ( R1 ` y ) )
13 12 3adant1 
 |-  ( ( x e. On /\ y e. On /\ x e. y ) -> -. ( R1 ` x ) = ( R1 ` y ) )
14 13 pm2.21d 
 |-  ( ( x e. On /\ y e. On /\ x e. y ) -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) )
15 14 3expia 
 |-  ( ( x e. On /\ y e. On ) -> ( x e. y -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) ) )
16 ax1w 
 |-  ( ( x e. On /\ y e. On ) -> ( x = y -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) ) )
17 r1sdom 
 |-  ( ( x e. On /\ y e. x ) -> ( R1 ` y ) ~< ( R1 ` x ) )
18 breq2 
 |-  ( ( R1 ` x ) = ( R1 ` y ) -> ( ( R1 ` y ) ~< ( R1 ` x ) <-> ( R1 ` y ) ~< ( R1 ` y ) ) )
19 17 18 syl5ibcom 
 |-  ( ( x e. On /\ y e. x ) -> ( ( R1 ` x ) = ( R1 ` y ) -> ( R1 ` y ) ~< ( R1 ` y ) ) )
20 8 19 mtoi 
 |-  ( ( x e. On /\ y e. x ) -> -. ( R1 ` x ) = ( R1 ` y ) )
21 20 3adant2 
 |-  ( ( x e. On /\ y e. On /\ y e. x ) -> -. ( R1 ` x ) = ( R1 ` y ) )
22 21 pm2.21d 
 |-  ( ( x e. On /\ y e. On /\ y e. x ) -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) )
23 22 3expia 
 |-  ( ( x e. On /\ y e. On ) -> ( y e. x -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) ) )
24 15 16 23 3jaod 
 |-  ( ( x e. On /\ y e. On ) -> ( ( x e. y \/ x = y \/ y e. x ) -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) ) )
25 7 24 mpd 
 |-  ( ( x e. On /\ y e. On ) -> ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) )
26 25 rgen2 
 |-  A. x e. On A. y e. On ( ( R1 ` x ) = ( R1 ` y ) -> x = y )
27 dff13 
 |-  ( R1 : On -1-1-> _V <-> ( R1 : On --> _V /\ A. x e. On A. y e. On ( ( R1 ` x ) = ( R1 ` y ) -> x = y ) ) )
28 3 26 27 mpbir2an 
 |-  R1 : On -1-1-> _V