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 syl5bi
 |-  ( ( 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 ) )