Metamath Proof Explorer

Theorem rankeq1o

Description: The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015)

Ref Expression
Assertion rankeq1o 
|- ( ( rank ` A ) = 1o <-> A = { (/) } )

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 neeq1 
 |-  ( ( rank ` A ) = 1o -> ( ( rank ` A ) =/= (/) <-> 1o =/= (/) ) )
3 1 2 mpbiri 
 |-  ( ( rank ` A ) = 1o -> ( rank ` A ) =/= (/) )
4 3 neneqd 
 |-  ( ( rank ` A ) = 1o -> -. ( rank ` A ) = (/) )
5 fvprc 
 |-  ( -. A e. _V -> ( rank ` A ) = (/) )
6 4 5 nsyl2 
 |-  ( ( rank ` A ) = 1o -> A e. _V )
7 fveqeq2 
 |-  ( x = A -> ( ( rank ` x ) = 1o <-> ( rank ` A ) = 1o ) )
8 eqeq1 
 |-  ( x = A -> ( x = 1o <-> A = 1o ) )
9 7 8 imbi12d 
 |-  ( x = A -> ( ( ( rank ` x ) = 1o -> x = 1o ) <-> ( ( rank ` A ) = 1o -> A = 1o ) ) )
10 neeq1 
 |-  ( ( rank ` x ) = 1o -> ( ( rank ` x ) =/= (/) <-> 1o =/= (/) ) )
11 1 10 mpbiri 
 |-  ( ( rank ` x ) = 1o -> ( rank ` x ) =/= (/) )
12 vex 
 |-  x e. _V
13 12 rankeq0 
 |-  ( x = (/) <-> ( rank ` x ) = (/) )
14 13 necon3bii 
 |-  ( x =/= (/) <-> ( rank ` x ) =/= (/) )
15 11 14 sylibr 
 |-  ( ( rank ` x ) = 1o -> x =/= (/) )
16 12 rankval 
 |-  ( rank ` x ) = |^| { y e. On | x e. ( R1 ` suc y ) }
17 16 eqeq1i 
 |-  ( ( rank ` x ) = 1o <-> |^| { y e. On | x e. ( R1 ` suc y ) } = 1o )
18 ssrab2 
 |-  { y e. On | x e. ( R1 ` suc y ) } C_ On
19 elirr 
 |-  -. 1o e. 1o
20 1oex 
 |-  1o e. _V
21 id 
 |-  ( _V = 1o -> _V = 1o )
22 20 21 eleqtrid 
 |-  ( _V = 1o -> 1o e. 1o )
23 19 22 mto 
 |-  -. _V = 1o
24 inteq 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } = (/) -> |^| { y e. On | x e. ( R1 ` suc y ) } = |^| (/) )
25 int0 
 |-  |^| (/) = _V
26 24 25 eqtrdi 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } = (/) -> |^| { y e. On | x e. ( R1 ` suc y ) } = _V )
27 26 eqeq1d 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } = (/) -> ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o <-> _V = 1o ) )
28 23 27 mtbiri 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } = (/) -> -. |^| { y e. On | x e. ( R1 ` suc y ) } = 1o )
29 28 necon2ai 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o -> { y e. On | x e. ( R1 ` suc y ) } =/= (/) )
30 onint 
 |-  ( ( { y e. On | x e. ( R1 ` suc y ) } C_ On /\ { y e. On | x e. ( R1 ` suc y ) } =/= (/) ) -> |^| { y e. On | x e. ( R1 ` suc y ) } e. { y e. On | x e. ( R1 ` suc y ) } )
31 18 29 30 sylancr 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o -> |^| { y e. On | x e. ( R1 ` suc y ) } e. { y e. On | x e. ( R1 ` suc y ) } )
32 eleq1 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o -> ( |^| { y e. On | x e. ( R1 ` suc y ) } e. { y e. On | x e. ( R1 ` suc y ) } <-> 1o e. { y e. On | x e. ( R1 ` suc y ) } ) )
33 31 32 mpbid 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o -> 1o e. { y e. On | x e. ( R1 ` suc y ) } )
34 suceq 
 |-  ( y = 1o -> suc y = suc 1o )
35 34 fveq2d 
 |-  ( y = 1o -> ( R1 ` suc y ) = ( R1 ` suc 1o ) )
36 df-1o 
 |-  1o = suc (/)
37 36 fveq2i 
 |-  ( R1 ` 1o ) = ( R1 ` suc (/) )
38 0elon 
 |-  (/) e. On
39 r1suc 
 |-  ( (/) e. On -> ( R1 ` suc (/) ) = ~P ( R1 ` (/) ) )
40 38 39 ax-mp 
 |-  ( R1 ` suc (/) ) = ~P ( R1 ` (/) )
41 r10 
 |-  ( R1 ` (/) ) = (/)
42 41 pweqi 
 |-  ~P ( R1 ` (/) ) = ~P (/)
43 37 40 42 3eqtri 
 |-  ( R1 ` 1o ) = ~P (/)
44 43 pweqi 
 |-  ~P ( R1 ` 1o ) = ~P ~P (/)
45 pw0 
 |-  ~P (/) = { (/) }
46 45 pweqi 
 |-  ~P ~P (/) = ~P { (/) }
47 pwpw0 
 |-  ~P { (/) } = { (/) , { (/) } }
48 44 46 47 3eqtrri 
 |-  { (/) , { (/) } } = ~P ( R1 ` 1o )
49 1on 
 |-  1o e. On
50 r1suc 
 |-  ( 1o e. On -> ( R1 ` suc 1o ) = ~P ( R1 ` 1o ) )
51 49 50 ax-mp 
 |-  ( R1 ` suc 1o ) = ~P ( R1 ` 1o )
52 48 51 eqtr4i 
 |-  { (/) , { (/) } } = ( R1 ` suc 1o )
53 35 52 eqtr4di 
 |-  ( y = 1o -> ( R1 ` suc y ) = { (/) , { (/) } } )
54 53 eleq2d 
 |-  ( y = 1o -> ( x e. ( R1 ` suc y ) <-> x e. { (/) , { (/) } } ) )
55 54 elrab 
 |-  ( 1o e. { y e. On | x e. ( R1 ` suc y ) } <-> ( 1o e. On /\ x e. { (/) , { (/) } } ) )
56 33 55 sylib 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o -> ( 1o e. On /\ x e. { (/) , { (/) } } ) )
57 12 elpr 
 |-  ( x e. { (/) , { (/) } } <-> ( x = (/) \/ x = { (/) } ) )
58 df-ne 
 |-  ( x =/= (/) <-> -. x = (/) )
59 orel1 
 |-  ( -. x = (/) -> ( ( x = (/) \/ x = { (/) } ) -> x = { (/) } ) )
60 58 59 sylbi 
 |-  ( x =/= (/) -> ( ( x = (/) \/ x = { (/) } ) -> x = { (/) } ) )
61 df1o2 
 |-  1o = { (/) }
62 eqeq2 
 |-  ( x = { (/) } -> ( 1o = x <-> 1o = { (/) } ) )
63 61 62 mpbiri 
 |-  ( x = { (/) } -> 1o = x )
64 63 eqcomd 
 |-  ( x = { (/) } -> x = 1o )
65 60 64 syl6com 
 |-  ( ( x = (/) \/ x = { (/) } ) -> ( x =/= (/) -> x = 1o ) )
66 57 65 sylbi 
 |-  ( x e. { (/) , { (/) } } -> ( x =/= (/) -> x = 1o ) )
67 66 adantl 
 |-  ( ( 1o e. On /\ x e. { (/) , { (/) } } ) -> ( x =/= (/) -> x = 1o ) )
68 56 67 syl 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } = 1o -> ( x =/= (/) -> x = 1o ) )
69 17 68 sylbi 
 |-  ( ( rank ` x ) = 1o -> ( x =/= (/) -> x = 1o ) )
70 15 69 mpd 
 |-  ( ( rank ` x ) = 1o -> x = 1o )
71 9 70 vtoclg 
 |-  ( A e. _V -> ( ( rank ` A ) = 1o -> A = 1o ) )
72 6 71 mpcom 
 |-  ( ( rank ` A ) = 1o -> A = 1o )
73 fveq2 
 |-  ( A = 1o -> ( rank ` A ) = ( rank ` 1o ) )
74 r111 
 |-  R1 : On -1-1-> _V
75 f1dm 
 |-  ( R1 : On -1-1-> _V -> dom R1 = On )
76 74 75 ax-mp 
 |-  dom R1 = On
77 49 76 eleqtrri 
 |-  1o e. dom R1
78 rankonid 
 |-  ( 1o e. dom R1 <-> ( rank ` 1o ) = 1o )
79 77 78 mpbi 
 |-  ( rank ` 1o ) = 1o
80 73 79 eqtrdi 
 |-  ( A = 1o -> ( rank ` A ) = 1o )
81 72 80 impbii 
 |-  ( ( rank ` A ) = 1o <-> A = 1o )
82 61 eqeq2i 
 |-  ( A = 1o <-> A = { (/) } )
83 81 82 bitri 
 |-  ( ( rank ` A ) = 1o <-> A = { (/) } )