Metamath Proof Explorer

Theorem gruina

Description: If a Grothendieck universe U is nonempty, then the height of the ordinals in U is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 gruina.1 
 |-  A = ( U i^i On )
2 n0 
 |-  ( U =/= (/) <-> E. x x e. U )
3 0ss 
 |-  (/) C_ x
4 gruss 
 |-  ( ( U e. Univ /\ x e. U /\ (/) C_ x ) -> (/) e. U )
5 3 4 mp3an3 
 |-  ( ( U e. Univ /\ x e. U ) -> (/) e. U )
6 0elon 
 |-  (/) e. On
7 elin 
 |-  ( (/) e. ( U i^i On ) <-> ( (/) e. U /\ (/) e. On ) )
8 5 6 7 sylanblrc 
 |-  ( ( U e. Univ /\ x e. U ) -> (/) e. ( U i^i On ) )
9 8 1 eleqtrrdi 
 |-  ( ( U e. Univ /\ x e. U ) -> (/) e. A )
10 9 ne0d 
 |-  ( ( U e. Univ /\ x e. U ) -> A =/= (/) )
11 10 expcom 
 |-  ( x e. U -> ( U e. Univ -> A =/= (/) ) )
12 11 exlimiv 
 |-  ( E. x x e. U -> ( U e. Univ -> A =/= (/) ) )
13 2 12 sylbi 
 |-  ( U =/= (/) -> ( U e. Univ -> A =/= (/) ) )
14 13 impcom 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> A =/= (/) )
15 grutr 
 |-  ( U e. Univ -> Tr U )
16 tron 
 |-  Tr On
17 trin 
 |-  ( ( Tr U /\ Tr On ) -> Tr ( U i^i On ) )
18 15 16 17 sylancl 
 |-  ( U e. Univ -> Tr ( U i^i On ) )
19 inss2 
 |-  ( U i^i On ) C_ On
20 epweon 
 |-  _E We On
21 wess 
 |-  ( ( U i^i On ) C_ On -> ( _E We On -> _E We ( U i^i On ) ) )
22 19 20 21 mp2 
 |-  _E We ( U i^i On )
23 df-ord 
 |-  ( Ord ( U i^i On ) <-> ( Tr ( U i^i On ) /\ _E We ( U i^i On ) ) )
24 18 22 23 sylanblrc 
 |-  ( U e. Univ -> Ord ( U i^i On ) )
25 inex1g 
 |-  ( U e. Univ -> ( U i^i On ) e. _V )
26 elon2 
 |-  ( ( U i^i On ) e. On <-> ( Ord ( U i^i On ) /\ ( U i^i On ) e. _V ) )
27 24 25 26 sylanbrc 
 |-  ( U e. Univ -> ( U i^i On ) e. On )
28 1 27 eqeltrid 
 |-  ( U e. Univ -> A e. On )
29 28 adantr 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> A e. On )
30 eloni 
 |-  ( A e. On -> Ord A )
31 ordirr 
 |-  ( Ord A -> -. A e. A )
32 30 31 syl 
 |-  ( A e. On -> -. A e. A )
33 elin 
 |-  ( A e. ( U i^i On ) <-> ( A e. U /\ A e. On ) )
34 33 biimpri 
 |-  ( ( A e. U /\ A e. On ) -> A e. ( U i^i On ) )
35 34 1 eleqtrrdi 
 |-  ( ( A e. U /\ A e. On ) -> A e. A )
36 35 expcom 
 |-  ( A e. On -> ( A e. U -> A e. A ) )
37 32 36 mtod 
 |-  ( A e. On -> -. A e. U )
38 29 37 syl 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> -. A e. U )
39 inss1 
 |-  ( U i^i On ) C_ U
40 1 39 eqsstri 
 |-  A C_ U
41 40 sseli 
 |-  ( x e. A -> x e. U )
42 vpwex 
 |-  ~P x e. _V
43 42 canth2 
 |-  ~P x ~< ~P ~P x
44 42 pwex 
 |-  ~P ~P x e. _V
45 44 cardid 
 |-  ( card ` ~P ~P x ) ~~ ~P ~P x
46 45 ensymi 
 |-  ~P ~P x ~~ ( card ` ~P ~P x )
47 28 adantr 
 |-  ( ( U e. Univ /\ x e. U ) -> A e. On )
48 grupw 
 |-  ( ( U e. Univ /\ x e. U ) -> ~P x e. U )
49 grupw 
 |-  ( ( U e. Univ /\ ~P x e. U ) -> ~P ~P x e. U )
50 48 49 syldan 
 |-  ( ( U e. Univ /\ x e. U ) -> ~P ~P x e. U )
51 28 adantr 
 |-  ( ( U e. Univ /\ ~P ~P x e. U ) -> A e. On )
52 endom 
 |-  ( ( card ` ~P ~P x ) ~~ ~P ~P x -> ( card ` ~P ~P x ) ~<_ ~P ~P x )
53 45 52 ax-mp 
 |-  ( card ` ~P ~P x ) ~<_ ~P ~P x
54 cardon 
 |-  ( card ` ~P ~P x ) e. On
55 grudomon 
 |-  ( ( U e. Univ /\ ( card ` ~P ~P x ) e. On /\ ( ~P ~P x e. U /\ ( card ` ~P ~P x ) ~<_ ~P ~P x ) ) -> ( card ` ~P ~P x ) e. U )
56 54 55 mp3an2 
 |-  ( ( U e. Univ /\ ( ~P ~P x e. U /\ ( card ` ~P ~P x ) ~<_ ~P ~P x ) ) -> ( card ` ~P ~P x ) e. U )
57 53 56 mpanr2 
 |-  ( ( U e. Univ /\ ~P ~P x e. U ) -> ( card ` ~P ~P x ) e. U )
58 elin 
 |-  ( ( card ` ~P ~P x ) e. ( U i^i On ) <-> ( ( card ` ~P ~P x ) e. U /\ ( card ` ~P ~P x ) e. On ) )
59 58 biimpri 
 |-  ( ( ( card ` ~P ~P x ) e. U /\ ( card ` ~P ~P x ) e. On ) -> ( card ` ~P ~P x ) e. ( U i^i On ) )
60 59 1 eleqtrrdi 
 |-  ( ( ( card ` ~P ~P x ) e. U /\ ( card ` ~P ~P x ) e. On ) -> ( card ` ~P ~P x ) e. A )
61 57 54 60 sylancl 
 |-  ( ( U e. Univ /\ ~P ~P x e. U ) -> ( card ` ~P ~P x ) e. A )
62 onelss 
 |-  ( A e. On -> ( ( card ` ~P ~P x ) e. A -> ( card ` ~P ~P x ) C_ A ) )
63 51 61 62 sylc 
 |-  ( ( U e. Univ /\ ~P ~P x e. U ) -> ( card ` ~P ~P x ) C_ A )
64 50 63 syldan 
 |-  ( ( U e. Univ /\ x e. U ) -> ( card ` ~P ~P x ) C_ A )
65 ssdomg 
 |-  ( A e. On -> ( ( card ` ~P ~P x ) C_ A -> ( card ` ~P ~P x ) ~<_ A ) )
66 47 64 65 sylc 
 |-  ( ( U e. Univ /\ x e. U ) -> ( card ` ~P ~P x ) ~<_ A )
67 endomtr 
 |-  ( ( ~P ~P x ~~ ( card ` ~P ~P x ) /\ ( card ` ~P ~P x ) ~<_ A ) -> ~P ~P x ~<_ A )
68 46 66 67 sylancr 
 |-  ( ( U e. Univ /\ x e. U ) -> ~P ~P x ~<_ A )
69 sdomdomtr 
 |-  ( ( ~P x ~< ~P ~P x /\ ~P ~P x ~<_ A ) -> ~P x ~< A )
70 43 68 69 sylancr 
 |-  ( ( U e. Univ /\ x e. U ) -> ~P x ~< A )
71 41 70 sylan2 
 |-  ( ( U e. Univ /\ x e. A ) -> ~P x ~< A )
72 71 ralrimiva 
 |-  ( U e. Univ -> A. x e. A ~P x ~< A )
73 inawinalem 
 |-  ( A e. On -> ( A. x e. A ~P x ~< A -> A. x e. A E. y e. A x ~< y ) )
74 28 72 73 sylc 
 |-  ( U e. Univ -> A. x e. A E. y e. A x ~< y )
75 74 adantr 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> A. x e. A E. y e. A x ~< y )
76 winainflem 
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> _om C_ A )
77 14 29 75 76 syl3anc 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> _om C_ A )
78 vex 
 |-  x e. _V
79 78 canth2 
 |-  x ~< ~P x
80 sdomtr 
 |-  ( ( x ~< ~P x /\ ~P x ~< A ) -> x ~< A )
81 79 71 80 sylancr 
 |-  ( ( U e. Univ /\ x e. A ) -> x ~< A )
82 81 ralrimiva 
 |-  ( U e. Univ -> A. x e. A x ~< A )
83 iscard 
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A x ~< A ) )
84 28 82 83 sylanbrc 
 |-  ( U e. Univ -> ( card ` A ) = A )
85 cardlim 
 |-  ( _om C_ ( card ` A ) <-> Lim ( card ` A ) )
86 sseq2 
 |-  ( ( card ` A ) = A -> ( _om C_ ( card ` A ) <-> _om C_ A ) )
87 limeq 
 |-  ( ( card ` A ) = A -> ( Lim ( card ` A ) <-> Lim A ) )
88 86 87 bibi12d 
 |-  ( ( card ` A ) = A -> ( ( _om C_ ( card ` A ) <-> Lim ( card ` A ) ) <-> ( _om C_ A <-> Lim A ) ) )
89 85 88 mpbii 
 |-  ( ( card ` A ) = A -> ( _om C_ A <-> Lim A ) )
90 84 89 syl 
 |-  ( U e. Univ -> ( _om C_ A <-> Lim A ) )
91 90 adantr 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( _om C_ A <-> Lim A ) )
92 77 91 mpbid 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> Lim A )
93 cflm 
 |-  ( ( A e. On /\ Lim A ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
94 29 92 93 syl2anc 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( cf ` A ) = |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
95 cardon 
 |-  ( card ` y ) e. On
96 eleq1 
 |-  ( x = ( card ` y ) -> ( x e. On <-> ( card ` y ) e. On ) )
97 95 96 mpbiri 
 |-  ( x = ( card ` y ) -> x e. On )
98 97 adantr 
 |-  ( ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) -> x e. On )
99 98 exlimiv 
 |-  ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) -> x e. On )
100 99 abssi 
 |-  { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ On
101 fvex 
 |-  ( cf ` A ) e. _V
102 94 101 eqeltrrdi 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } e. _V )
103 intex 
 |-  ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } =/= (/) <-> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } e. _V )
104 102 103 sylibr 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } =/= (/) )
105 onint 
 |-  ( ( { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } C_ On /\ { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } =/= (/) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
106 100 104 105 sylancr 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> |^| { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
107 94 106 eqeltrd 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } )
108 eqeq1 
 |-  ( x = ( cf ` A ) -> ( x = ( card ` y ) <-> ( cf ` A ) = ( card ` y ) ) )
109 108 anbi1d 
 |-  ( x = ( cf ` A ) -> ( ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) <-> ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) ) )
110 109 exbidv 
 |-  ( x = ( cf ` A ) -> ( E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) <-> E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) ) )
111 101 110 elab 
 |-  ( ( cf ` A ) e. { x | E. y ( x = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) } <-> E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) )
112 107 111 sylib 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) )
113 simp2rr 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> A = U. y )
114 simp1l 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> U e. Univ )
115 simp2rl 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> y C_ A )
116 115 40 sstrdi 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> y C_ U )
117 40 sseli 
 |-  ( ( cf ` A ) e. A -> ( cf ` A ) e. U )
118 117 3ad2ant3 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> ( cf ` A ) e. U )
119 simp2l 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> ( cf ` A ) = ( card ` y ) )
120 vex 
 |-  y e. _V
121 120 cardid 
 |-  ( card ` y ) ~~ y
122 119 121 eqbrtrdi 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> ( cf ` A ) ~~ y )
123 gruen 
 |-  ( ( U e. Univ /\ y C_ U /\ ( ( cf ` A ) e. U /\ ( cf ` A ) ~~ y ) ) -> y e. U )
124 114 116 118 122 123 syl112anc 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> y e. U )
125 gruuni 
 |-  ( ( U e. Univ /\ y e. U ) -> U. y e. U )
126 114 124 125 syl2anc 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> U. y e. U )
127 113 126 eqeltrd 
 |-  ( ( ( U e. Univ /\ U =/= (/) ) /\ ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) /\ ( cf ` A ) e. A ) -> A e. U )
128 127 3exp 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) -> ( ( cf ` A ) e. A -> A e. U ) ) )
129 128 exlimdv 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( E. y ( ( cf ` A ) = ( card ` y ) /\ ( y C_ A /\ A = U. y ) ) -> ( ( cf ` A ) e. A -> A e. U ) ) )
130 112 129 mpd 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( ( cf ` A ) e. A -> A e. U ) )
131 38 130 mtod 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> -. ( cf ` A ) e. A )
132 cfon 
 |-  ( cf ` A ) e. On
133 cfle 
 |-  ( cf ` A ) C_ A
134 onsseleq 
 |-  ( ( ( cf ` A ) e. On /\ A e. On ) -> ( ( cf ` A ) C_ A <-> ( ( cf ` A ) e. A \/ ( cf ` A ) = A ) ) )
135 133 134 mpbii 
 |-  ( ( ( cf ` A ) e. On /\ A e. On ) -> ( ( cf ` A ) e. A \/ ( cf ` A ) = A ) )
136 132 135 mpan 
 |-  ( A e. On -> ( ( cf ` A ) e. A \/ ( cf ` A ) = A ) )
137 136 ord 
 |-  ( A e. On -> ( -. ( cf ` A ) e. A -> ( cf ` A ) = A ) )
138 29 131 137 sylc 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> ( cf ` A ) = A )
139 72 adantr 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> A. x e. A ~P x ~< A )
140 elina 
 |-  ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) )
141 14 138 139 140 syl3anbrc 
 |-  ( ( U e. Univ /\ U =/= (/) ) -> A e. Inacc )