Metamath Proof Explorer

Theorem grur1

Description: A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis gruina.1 
|- A = ( U i^i On )
Assertion grur1 
|- ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> U = ( R1 ` A ) )

Proof

Step Hyp Ref Expression
1 gruina.1 
 |-  A = ( U i^i On )
2 nss 
 |-  ( -. U C_ ( R1 ` A ) <-> E. x ( x e. U /\ -. x e. ( R1 ` A ) ) )
3 fveqeq2 
 |-  ( y = x -> ( ( rank ` y ) = A <-> ( rank ` x ) = A ) )
4 3 rspcev 
 |-  ( ( x e. U /\ ( rank ` x ) = A ) -> E. y e. U ( rank ` y ) = A )
5 4 ex 
 |-  ( x e. U -> ( ( rank ` x ) = A -> E. y e. U ( rank ` y ) = A ) )
6 5 ad2antrl 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( ( rank ` x ) = A -> E. y e. U ( rank ` y ) = A ) )
7 simplr 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> U e. U. ( R1 " On ) )
8 simprl 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> x e. U )
9 r1elssi 
 |-  ( U e. U. ( R1 " On ) -> U C_ U. ( R1 " On ) )
10 9 sseld 
 |-  ( U e. U. ( R1 " On ) -> ( x e. U -> x e. U. ( R1 " On ) ) )
11 7 8 10 sylc 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> x e. U. ( R1 " On ) )
12 tcrank 
 |-  ( x e. U. ( R1 " On ) -> ( rank ` x ) = ( rank " ( TC ` x ) ) )
13 11 12 syl 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( rank ` x ) = ( rank " ( TC ` x ) ) )
14 13 eleq2d 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( A e. ( rank ` x ) <-> A e. ( rank " ( TC ` x ) ) ) )
15 gruelss 
 |-  ( ( U e. Univ /\ x e. U ) -> x C_ U )
16 grutr 
 |-  ( U e. Univ -> Tr U )
17 16 adantr 
 |-  ( ( U e. Univ /\ x e. U ) -> Tr U )
18 vex 
 |-  x e. _V
19 tcmin 
 |-  ( x e. _V -> ( ( x C_ U /\ Tr U ) -> ( TC ` x ) C_ U ) )
20 18 19 ax-mp 
 |-  ( ( x C_ U /\ Tr U ) -> ( TC ` x ) C_ U )
21 15 17 20 syl2anc 
 |-  ( ( U e. Univ /\ x e. U ) -> ( TC ` x ) C_ U )
22 rankf 
 |-  rank : U. ( R1 " On ) --> On
23 ffun 
 |-  ( rank : U. ( R1 " On ) --> On -> Fun rank )
24 22 23 ax-mp 
 |-  Fun rank
25 fvelima 
 |-  ( ( Fun rank /\ A e. ( rank " ( TC ` x ) ) ) -> E. y e. ( TC ` x ) ( rank ` y ) = A )
26 24 25 mpan 
 |-  ( A e. ( rank " ( TC ` x ) ) -> E. y e. ( TC ` x ) ( rank ` y ) = A )
27 ssrexv 
 |-  ( ( TC ` x ) C_ U -> ( E. y e. ( TC ` x ) ( rank ` y ) = A -> E. y e. U ( rank ` y ) = A ) )
28 21 26 27 syl2im 
 |-  ( ( U e. Univ /\ x e. U ) -> ( A e. ( rank " ( TC ` x ) ) -> E. y e. U ( rank ` y ) = A ) )
29 28 ad2ant2r 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( A e. ( rank " ( TC ` x ) ) -> E. y e. U ( rank ` y ) = A ) )
30 14 29 sylbid 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( A e. ( rank ` x ) -> E. y e. U ( rank ` y ) = A ) )
31 simprr 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> -. x e. ( R1 ` A ) )
32 ne0i 
 |-  ( x e. U -> U =/= (/) )
33 1 gruina 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> A e. Inacc )
34 32 33 sylan2 
 |-  ( ( U e. Univ /\ x e. U ) -> A e. Inacc )
35 inawina 
 |-  ( A e. Inacc -> A e. InaccW )
36 winaon 
 |-  ( A e. InaccW -> A e. On )
37 34 35 36 3syl 
 |-  ( ( U e. Univ /\ x e. U ) -> A e. On )
38 r1fnon 
 |-  R1 Fn On
39 fndm 
 |-  ( R1 Fn On -> dom R1 = On )
40 38 39 ax-mp 
 |-  dom R1 = On
41 37 40 eleqtrrdi 
 |-  ( ( U e. Univ /\ x e. U ) -> A e. dom R1 )
42 41 ad2ant2r 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> A e. dom R1 )
43 rankr1ag 
 |-  ( ( x e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
44 11 42 43 syl2anc 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
45 31 44 mtbid 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> -. ( rank ` x ) e. A )
46 rankon 
 |-  ( rank ` x ) e. On
47 eloni 
 |-  ( ( rank ` x ) e. On -> Ord ( rank ` x ) )
48 eloni 
 |-  ( A e. On -> Ord A )
49 ordtri3or 
 |-  ( ( Ord ( rank ` x ) /\ Ord A ) -> ( ( rank ` x ) e. A \/ ( rank ` x ) = A \/ A e. ( rank ` x ) ) )
50 47 48 49 syl2an 
 |-  ( ( ( rank ` x ) e. On /\ A e. On ) -> ( ( rank ` x ) e. A \/ ( rank ` x ) = A \/ A e. ( rank ` x ) ) )
51 46 37 50 sylancr 
 |-  ( ( U e. Univ /\ x e. U ) -> ( ( rank ` x ) e. A \/ ( rank ` x ) = A \/ A e. ( rank ` x ) ) )
52 3orass 
 |-  ( ( ( rank ` x ) e. A \/ ( rank ` x ) = A \/ A e. ( rank ` x ) ) <-> ( ( rank ` x ) e. A \/ ( ( rank ` x ) = A \/ A e. ( rank ` x ) ) ) )
53 51 52 sylib 
 |-  ( ( U e. Univ /\ x e. U ) -> ( ( rank ` x ) e. A \/ ( ( rank ` x ) = A \/ A e. ( rank ` x ) ) ) )
54 53 ord 
 |-  ( ( U e. Univ /\ x e. U ) -> ( -. ( rank ` x ) e. A -> ( ( rank ` x ) = A \/ A e. ( rank ` x ) ) ) )
55 54 ad2ant2r 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( -. ( rank ` x ) e. A -> ( ( rank ` x ) = A \/ A e. ( rank ` x ) ) ) )
56 45 55 mpd 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> ( ( rank ` x ) = A \/ A e. ( rank ` x ) ) )
57 6 30 56 mpjaod 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( x e. U /\ -. x e. ( R1 ` A ) ) ) -> E. y e. U ( rank ` y ) = A )
58 57 ex 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> ( ( x e. U /\ -. x e. ( R1 ` A ) ) -> E. y e. U ( rank ` y ) = A ) )
59 58 exlimdv 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> ( E. x ( x e. U /\ -. x e. ( R1 ` A ) ) -> E. y e. U ( rank ` y ) = A ) )
60 2 59 biimtrid 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> ( -. U C_ ( R1 ` A ) -> E. y e. U ( rank ` y ) = A ) )
61 simpll 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> U e. Univ )
62 ne0i 
 |-  ( y e. U -> U =/= (/) )
63 62 33 sylan2 
 |-  ( ( U e. Univ /\ y e. U ) -> A e. Inacc )
64 63 ad2ant2r 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> A e. Inacc )
65 64 35 36 3syl 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> A e. On )
66 simprl 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> y e. U )
67 fveq2 
 |-  ( ( rank ` y ) = A -> ( cf ` ( rank ` y ) ) = ( cf ` A ) )
68 67 ad2antll 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> ( cf ` ( rank ` y ) ) = ( cf ` A ) )
69 elina 
 |-  ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) )
70 69 simp2bi 
 |-  ( A e. Inacc -> ( cf ` A ) = A )
71 64 70 syl 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> ( cf ` A ) = A )
72 68 71 eqtrd 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> ( cf ` ( rank ` y ) ) = A )
73 rankcf 
 |-  -. y ~< ( cf ` ( rank ` y ) )
74 fvex 
 |-  ( cf ` ( rank ` y ) ) e. _V
75 vex 
 |-  y e. _V
76 domtri 
 |-  ( ( ( cf ` ( rank ` y ) ) e. _V /\ y e. _V ) -> ( ( cf ` ( rank ` y ) ) ~<_ y <-> -. y ~< ( cf ` ( rank ` y ) ) ) )
77 74 75 76 mp2an 
 |-  ( ( cf ` ( rank ` y ) ) ~<_ y <-> -. y ~< ( cf ` ( rank ` y ) ) )
78 73 77 mpbir 
 |-  ( cf ` ( rank ` y ) ) ~<_ y
79 72 78 eqbrtrrdi 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> A ~<_ y )
80 grudomon 
 |-  ( ( U e. Univ /\ A e. On /\ ( y e. U /\ A ~<_ y ) ) -> A e. U )
81 61 65 66 79 80 syl112anc 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> A e. U )
82 elin 
 |-  ( A e. ( U i^i On ) <-> ( A e. U /\ A e. On ) )
83 82 biimpri 
 |-  ( ( A e. U /\ A e. On ) -> A e. ( U i^i On ) )
84 83 1 eleqtrrdi 
 |-  ( ( A e. U /\ A e. On ) -> A e. A )
85 ordirr 
 |-  ( Ord A -> -. A e. A )
86 48 85 syl 
 |-  ( A e. On -> -. A e. A )
87 86 adantl 
 |-  ( ( A e. U /\ A e. On ) -> -. A e. A )
88 84 87 pm2.21dd 
 |-  ( ( A e. U /\ A e. On ) -> U C_ ( R1 ` A ) )
89 81 65 88 syl2anc 
 |-  ( ( ( U e. Univ /\ U e. U. ( R1 " On ) ) /\ ( y e. U /\ ( rank ` y ) = A ) ) -> U C_ ( R1 ` A ) )
90 89 rexlimdvaa 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> ( E. y e. U ( rank ` y ) = A -> U C_ ( R1 ` A ) ) )
91 60 90 syld 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> ( -. U C_ ( R1 ` A ) -> U C_ ( R1 ` A ) ) )
92 91 pm2.18d 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> U C_ ( R1 ` A ) )
93 1 grur1a 
 |-  ( U e. Univ -> ( R1 ` A ) C_ U )
94 93 adantr 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> ( R1 ` A ) C_ U )
95 92 94 eqssd 
 |-  ( ( U e. Univ /\ U e. U. ( R1 " On ) ) -> U = ( R1 ` A ) )