MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gruina Unicode version

Theorem gruina 8456
Description: If a Grothendieck's universe  U is nonempty, then the height of the ordinals in  U is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013.)
Hypothesis
Ref Expression
gruina.1  |-  A  =  ( U  i^i  On )
Assertion
Ref Expression
gruina  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  A  e.  Inacc )

Proof of Theorem gruina
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0 3477 . . . 4  |-  ( U  =/=  (/)  <->  E. x  x  e.  U )
2 0ss 3496 . . . . . . . . . . 11  |-  (/)  C_  x
3 gruss 8434 . . . . . . . . . . 11  |-  ( ( U  e.  Univ  /\  x  e.  U  /\  (/)  C_  x
)  ->  (/)  e.  U
)
42, 3mp3an3 1266 . . . . . . . . . 10  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  (/)  e.  U
)
5 0elon 4461 . . . . . . . . . 10  |-  (/)  e.  On
64, 5jctir 524 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ( (/) 
e.  U  /\  (/)  e.  On ) )
7 elin 3371 . . . . . . . . 9  |-  ( (/)  e.  ( U  i^i  On ) 
<->  ( (/)  e.  U  /\  (/)  e.  On ) )
86, 7sylibr 203 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  (/)  e.  ( U  i^i  On ) )
9 gruina.1 . . . . . . . 8  |-  A  =  ( U  i^i  On )
108, 9syl6eleqr 2387 . . . . . . 7  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  (/)  e.  A
)
11 ne0i 3474 . . . . . . 7  |-  ( (/)  e.  A  ->  A  =/=  (/) )
1210, 11syl 15 . . . . . 6  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  A  =/=  (/) )
1312expcom 424 . . . . 5  |-  ( x  e.  U  ->  ( U  e.  Univ  ->  A  =/=  (/) ) )
1413exlimiv 1624 . . . 4  |-  ( E. x  x  e.  U  ->  ( U  e.  Univ  ->  A  =/=  (/) ) )
151, 14sylbi 187 . . 3  |-  ( U  =/=  (/)  ->  ( U  e.  Univ  ->  A  =/=  (/) ) )
1615impcom 419 . 2  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  A  =/=  (/) )
17 gruelss 8432 . . . . . . . . . 10  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  x  C_  U )
1817ralrimiva 2639 . . . . . . . . 9  |-  ( U  e.  Univ  ->  A. x  e.  U  x  C_  U
)
19 dftr3 4133 . . . . . . . . 9  |-  ( Tr  U  <->  A. x  e.  U  x  C_  U )
2018, 19sylibr 203 . . . . . . . 8  |-  ( U  e.  Univ  ->  Tr  U
)
21 tron 4431 . . . . . . . 8  |-  Tr  On
22 trin 4139 . . . . . . . 8  |-  ( ( Tr  U  /\  Tr  On )  ->  Tr  ( U  i^i  On ) )
2320, 21, 22sylancl 643 . . . . . . 7  |-  ( U  e.  Univ  ->  Tr  ( U  i^i  On ) )
24 inss2 3403 . . . . . . . . 9  |-  ( U  i^i  On )  C_  On
25 epweon 4591 . . . . . . . . 9  |-  _E  We  On
26 wess 4396 . . . . . . . . 9  |-  ( ( U  i^i  On ) 
C_  On  ->  (  _E  We  On  ->  _E  We  ( U  i^i  On ) ) )
2724, 25, 26mp2 17 . . . . . . . 8  |-  _E  We  ( U  i^i  On )
2827a1i 10 . . . . . . 7  |-  ( U  e.  Univ  ->  _E  We  ( U  i^i  On ) )
29 df-ord 4411 . . . . . . 7  |-  ( Ord  ( U  i^i  On ) 
<->  ( Tr  ( U  i^i  On )  /\  _E  We  ( U  i^i  On ) ) )
3023, 28, 29sylanbrc 645 . . . . . 6  |-  ( U  e.  Univ  ->  Ord  ( U  i^i  On ) )
31 inex1g 4173 . . . . . 6  |-  ( U  e.  Univ  ->  ( U  i^i  On )  e. 
_V )
32 elon2 4419 . . . . . 6  |-  ( ( U  i^i  On )  e.  On  <->  ( Ord  ( U  i^i  On )  /\  ( U  i^i  On )  e.  _V )
)
3330, 31, 32sylanbrc 645 . . . . 5  |-  ( U  e.  Univ  ->  ( U  i^i  On )  e.  On )
349, 33syl5eqel 2380 . . . 4  |-  ( U  e.  Univ  ->  A  e.  On )
3534adantr 451 . . 3  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  A  e.  On )
36 eloni 4418 . . . . . . 7  |-  ( A  e.  On  ->  Ord  A )
37 ordirr 4426 . . . . . . 7  |-  ( Ord 
A  ->  -.  A  e.  A )
3836, 37syl 15 . . . . . 6  |-  ( A  e.  On  ->  -.  A  e.  A )
39 elin 3371 . . . . . . . . 9  |-  ( A  e.  ( U  i^i  On )  <->  ( A  e.  U  /\  A  e.  On ) )
4039biimpri 197 . . . . . . . 8  |-  ( ( A  e.  U  /\  A  e.  On )  ->  A  e.  ( U  i^i  On ) )
4140, 9syl6eleqr 2387 . . . . . . 7  |-  ( ( A  e.  U  /\  A  e.  On )  ->  A  e.  A )
4241expcom 424 . . . . . 6  |-  ( A  e.  On  ->  ( A  e.  U  ->  A  e.  A ) )
4338, 42mtod 168 . . . . 5  |-  ( A  e.  On  ->  -.  A  e.  U )
4435, 43syl 15 . . . 4  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  -.  A  e.  U )
45 inss1 3402 . . . . . . . . . . . . . . . 16  |-  ( U  i^i  On )  C_  U
469, 45eqsstri 3221 . . . . . . . . . . . . . . 15  |-  A  C_  U
4746sseli 3189 . . . . . . . . . . . . . 14  |-  ( x  e.  A  ->  x  e.  U )
48 vex 2804 . . . . . . . . . . . . . . . . 17  |-  x  e. 
_V
4948pwex 4209 . . . . . . . . . . . . . . . 16  |-  ~P x  e.  _V
5049canth2 7030 . . . . . . . . . . . . . . 15  |-  ~P x  ~<  ~P ~P x
5149pwex 4209 . . . . . . . . . . . . . . . . . 18  |-  ~P ~P x  e.  _V
5251cardid 8185 . . . . . . . . . . . . . . . . 17  |-  ( card `  ~P ~P x ) 
~~  ~P ~P x
5352ensymi 6927 . . . . . . . . . . . . . . . 16  |-  ~P ~P x  ~~  ( card `  ~P ~P x )
5434adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  A  e.  On )
55 grupw 8433 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ~P x  e.  U )
56 grupw 8433 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  e.  Univ  /\  ~P x  e.  U )  ->  ~P ~P x  e.  U )
5755, 56syldan 456 . . . . . . . . . . . . . . . . . 18  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ~P ~P x  e.  U
)
5834adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  e.  Univ  /\  ~P ~P x  e.  U
)  ->  A  e.  On )
59 endom 6904 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
card `  ~P ~P x
)  ~~  ~P ~P x  ->  ( card `  ~P ~P x )  ~<_  ~P ~P x )
6052, 59ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( card `  ~P ~P x )  ~<_  ~P ~P x
61 cardon 7593 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( card `  ~P ~P x )  e.  On
62 grudomon 8455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 )
6361, 62mp3an2 1265 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( U  e.  Univ  /\  ( ~P ~P x  e.  U  /\  ( card `  ~P ~P x )  ~<_  ~P ~P x ) )  -> 
( card `  ~P ~P x
)  e.  U )
6460, 63mpanr2 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U  e.  Univ  /\  ~P ~P x  e.  U
)  ->  ( card `  ~P ~P x )  e.  U )
65 elin 3371 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
card `  ~P ~P x
)  e.  ( U  i^i  On )  <->  ( ( card `  ~P ~P x
)  e.  U  /\  ( card `  ~P ~P x
)  e.  On ) )
6665biimpri 197 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( card `  ~P ~P x )  e.  U  /\  ( card `  ~P ~P x )  e.  On )  ->  ( card `  ~P ~P x )  e.  ( U  i^i  On ) )
6766, 9syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( card `  ~P ~P x )  e.  U  /\  ( card `  ~P ~P x )  e.  On )  ->  ( card `  ~P ~P x )  e.  A
)
6864, 61, 67sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  e.  Univ  /\  ~P ~P x  e.  U
)  ->  ( card `  ~P ~P x )  e.  A )
69 onelss 4450 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  On  ->  (
( card `  ~P ~P x
)  e.  A  -> 
( card `  ~P ~P x
)  C_  A )
)
7058, 68, 69sylc 56 . . . . . . . . . . . . . . . . . 18  |-  ( ( U  e.  Univ  /\  ~P ~P x  e.  U
)  ->  ( card `  ~P ~P x ) 
C_  A )
7157, 70syldan 456 . . . . . . . . . . . . . . . . 17  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ( card `  ~P ~P x
)  C_  A )
72 ssdomg 6923 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  On  ->  (
( card `  ~P ~P x
)  C_  A  ->  (
card `  ~P ~P x
)  ~<_  A ) )
7354, 71, 72sylc 56 . . . . . . . . . . . . . . . 16  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ( card `  ~P ~P x
)  ~<_  A )
74 endomtr 6935 . . . . . . . . . . . . . . . 16  |-  ( ( ~P ~P x  ~~  ( card `  ~P ~P x
)  /\  ( card `  ~P ~P x )  ~<_  A )  ->  ~P ~P x  ~<_  A )
7553, 73, 74sylancr 644 . . . . . . . . . . . . . . 15  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ~P ~P x  ~<_  A )
76 sdomdomtr 7010 . . . . . . . . . . . . . . 15  |-  ( ( ~P x  ~<  ~P ~P x  /\  ~P ~P x  ~<_  A )  ->  ~P x  ~<  A )
7750, 75, 76sylancr 644 . . . . . . . . . . . . . 14  |-  ( ( U  e.  Univ  /\  x  e.  U )  ->  ~P x  ~<  A )
7847, 77sylan2 460 . . . . . . . . . . . . 13  |-  ( ( U  e.  Univ  /\  x  e.  A )  ->  ~P x  ~<  A )
7978ralrimiva 2639 . . . . . . . . . . . 12  |-  ( U  e.  Univ  ->  A. x  e.  A  ~P x  ~<  A )
80 inawinalem 8327 . . . . . . . . . . . 12  |-  ( A  e.  On  ->  ( A. x  e.  A  ~P x  ~<  A  ->  A. x  e.  A  E. y  e.  A  x  ~<  y ) )
8134, 79, 80sylc 56 . . . . . . . . . . 11  |-  ( U  e.  Univ  ->  A. x  e.  A  E. y  e.  A  x  ~<  y )
8281adantr 451 . . . . . . . . . 10  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  A. x  e.  A  E. y  e.  A  x  ~<  y )
83 winainflem 8331 . . . . . . . . . 10  |-  ( ( A  =/=  (/)  /\  A  e.  On  /\  A. x  e.  A  E. y  e.  A  x  ~<  y )  ->  om  C_  A
)
8416, 35, 82, 83syl3anc 1182 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  om  C_  A
)
8548canth2 7030 . . . . . . . . . . . . . 14  |-  x  ~<  ~P x
86 sdomtr 7015 . . . . . . . . . . . . . 14  |-  ( ( x  ~<  ~P x  /\  ~P x  ~<  A )  ->  x  ~<  A )
8785, 78, 86sylancr 644 . . . . . . . . . . . . 13  |-  ( ( U  e.  Univ  /\  x  e.  A )  ->  x  ~<  A )
8887ralrimiva 2639 . . . . . . . . . . . 12  |-  ( U  e.  Univ  ->  A. x  e.  A  x  ~<  A )
89 iscard 7624 . . . . . . . . . . . 12  |-  ( (
card `  A )  =  A  <->  ( A  e.  On  /\  A. x  e.  A  x  ~<  A ) )
9034, 88, 89sylanbrc 645 . . . . . . . . . . 11  |-  ( U  e.  Univ  ->  ( card `  A )  =  A )
91 cardlim 7621 . . . . . . . . . . . 12  |-  ( om  C_  ( card `  A
)  <->  Lim  ( card `  A
) )
92 sseq2 3213 . . . . . . . . . . . . 13  |-  ( (
card `  A )  =  A  ->  ( om  C_  ( card `  A
)  <->  om  C_  A )
)
93 limeq 4420 . . . . . . . . . . . . 13  |-  ( (
card `  A )  =  A  ->  ( Lim  ( card `  A
)  <->  Lim  A ) )
9492, 93bibi12d 312 . . . . . . . . . . . 12  |-  ( (
card `  A )  =  A  ->  ( ( om  C_  ( card `  A )  <->  Lim  ( card `  A ) )  <->  ( om  C_  A  <->  Lim  A ) ) )
9591, 94mpbii 202 . . . . . . . . . . 11  |-  ( (
card `  A )  =  A  ->  ( om  C_  A  <->  Lim  A ) )
9690, 95syl 15 . . . . . . . . . 10  |-  ( U  e.  Univ  ->  ( om  C_  A  <->  Lim  A ) )
9796adantr 451 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  ( om  C_  A  <->  Lim  A ) )
9884, 97mpbid 201 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  Lim  A )
99 cflm 7892 . . . . . . . 8  |-  ( ( A  e.  On  /\  Lim  A )  ->  ( cf `  A )  = 
|^| { x  |  E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) } )
10035, 98, 99syl2anc 642 . . . . . . 7  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  ( cf `  A )  = 
|^| { x  |  E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) } )
101 cardon 7593 . . . . . . . . . . . 12  |-  ( card `  y )  e.  On
102 eleq1 2356 . . . . . . . . . . . 12  |-  ( x  =  ( card `  y
)  ->  ( x  e.  On  <->  ( card `  y
)  e.  On ) )
103101, 102mpbiri 224 . . . . . . . . . . 11  |-  ( x  =  ( card `  y
)  ->  x  e.  On )
104103adantr 451 . . . . . . . . . 10  |-  ( ( x  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  ->  x  e.  On )
105104exlimiv 1624 . . . . . . . . 9  |-  ( E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) )  ->  x  e.  On )
106105abssi 3261 . . . . . . . 8  |-  { x  |  E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) }  C_  On
107 fvex 5555 . . . . . . . . . 10  |-  ( cf `  A )  e.  _V
108100, 107syl6eqelr 2385 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  |^| { x  |  E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) }  e.  _V )
109 intex 4183 . . . . . . . . 9  |-  ( { 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 )
110108, 109sylibr 203 . . . . . . . 8  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  { x  |  E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) }  =/=  (/) )
111 onint 4602 . . . . . . . 8  |-  ( ( { 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 ) ) } )
112106, 110, 111sylancr 644 . . . . . . 7  |-  ( ( 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 ) ) } )
113100, 112eqeltrd 2370 . . . . . 6  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  ( cf `  A )  e. 
{ x  |  E. y ( x  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) } )
114 eqeq1 2302 . . . . . . . . 9  |-  ( x  =  ( cf `  A
)  ->  ( x  =  ( card `  y
)  <->  ( cf `  A
)  =  ( card `  y ) ) )
115114anbi1d 685 . . . . . . . 8  |-  ( x  =  ( cf `  A
)  ->  ( (
x  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  <->  ( ( cf `  A )  =  ( card `  y
)  /\  ( y  C_  A  /\  A  = 
U. y ) ) ) )
116115exbidv 1616 . . . . . . 7  |-  ( 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 ) ) ) )
117107, 116elab 2927 . . . . . 6  |-  ( ( 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 ) ) )
118113, 117sylib 188 . . . . 5  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  E. y
( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) ) )
119 simp2rr 1025 . . . . . . . 8  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  A  =  U. y )
120 simp1l 979 . . . . . . . . 9  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  U  e.  Univ )
121 simp2rl 1024 . . . . . . . . . . 11  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  y  C_  A )
122121, 46syl6ss 3204 . . . . . . . . . 10  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  y  C_  U )
12346sseli 3189 . . . . . . . . . . 11  |-  ( ( cf `  A )  e.  A  ->  ( cf `  A )  e.  U )
1241233ad2ant3 978 . . . . . . . . . 10  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  ( cf `  A )  e.  U )
125 simp2l 981 . . . . . . . . . . 11  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  ( cf `  A )  =  ( card `  y
) )
126 vex 2804 . . . . . . . . . . . 12  |-  y  e. 
_V
127126cardid 8185 . . . . . . . . . . 11  |-  ( card `  y )  ~~  y
128125, 127syl6eqbr 4076 . . . . . . . . . 10  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  ( cf `  A )  ~~  y )
129 gruen 8450 . . . . . . . . . 10  |-  ( ( U  e.  Univ  /\  y  C_  U  /\  ( ( cf `  A )  e.  U  /\  ( cf `  A )  ~~  y ) )  -> 
y  e.  U )
130120, 122, 124, 128, 129syl112anc 1186 . . . . . . . . 9  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  y  e.  U )
131 gruuni 8438 . . . . . . . . 9  |-  ( ( U  e.  Univ  /\  y  e.  U )  ->  U. y  e.  U )
132120, 130, 131syl2anc 642 . . . . . . . 8  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  U. y  e.  U )
133119, 132eqeltrd 2370 . . . . . . 7  |-  ( ( ( U  e.  Univ  /\  U  =/=  (/) )  /\  ( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  /\  ( cf `  A )  e.  A )  ->  A  e.  U )
1341333exp 1150 . . . . . 6  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  (
( ( cf `  A
)  =  ( card `  y )  /\  (
y  C_  A  /\  A  =  U. y
) )  ->  (
( cf `  A
)  e.  A  ->  A  e.  U )
) )
135134exlimdv 1626 . . . . 5  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  ( E. y ( ( cf `  A )  =  (
card `  y )  /\  ( y  C_  A  /\  A  =  U. y ) )  -> 
( ( cf `  A
)  e.  A  ->  A  e.  U )
) )
136118, 135mpd 14 . . . 4  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  (
( cf `  A
)  e.  A  ->  A  e.  U )
)
13744, 136mtod 168 . . 3  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  -.  ( cf `  A )  e.  A )
138 cfon 7897 . . . . 5  |-  ( cf `  A )  e.  On
139 cfle 7896 . . . . . 6  |-  ( cf `  A )  C_  A
140 onsseleq 4449 . . . . . 6  |-  ( ( ( cf `  A
)  e.  On  /\  A  e.  On )  ->  ( ( cf `  A
)  C_  A  <->  ( ( cf `  A )  e.  A  \/  ( cf `  A )  =  A ) ) )
141139, 140mpbii 202 . . . . 5  |-  ( ( ( cf `  A
)  e.  On  /\  A  e.  On )  ->  ( ( cf `  A
)  e.  A  \/  ( cf `  A )  =  A ) )
142138, 141mpan 651 . . . 4  |-  ( A  e.  On  ->  (
( cf `  A
)  e.  A  \/  ( cf `  A )  =  A ) )
143142ord 366 . . 3  |-  ( A  e.  On  ->  ( -.  ( cf `  A
)  e.  A  -> 
( cf `  A
)  =  A ) )
14435, 137, 143sylc 56 . 2  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  ( cf `  A )  =  A )
14579adantr 451 . 2  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  A. x  e.  A  ~P x  ~<  A )
146 elina 8325 . 2  |-  ( A  e.  Inacc 
<->  ( A  =/=  (/)  /\  ( cf `  A )  =  A  /\  A. x  e.  A  ~P x  ~<  A ) )
14716, 144, 145, 146syl3anbrc 1136 1  |-  ( ( U  e.  Univ  /\  U  =/=  (/) )  ->  A  e.  Inacc )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282    =/= wne 2459   A.wral 2556   E.wrex 2557   _Vcvv 2801    i^i cin 3164    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   U.cuni 3843   |^|cint 3878   class class class wbr 4039   Tr wtr 4129    _E cep 4319    We wwe 4367   Ord word 4407   Oncon0 4408   Lim wlim 4409   omcom 4672   ` cfv 5271    ~~ cen 6876    ~<_ cdom 6877    ~< csdm 6878   cardccrd 7584   cfccf 7586   Inacccina 8321   Univcgru 8428
This theorem is referenced by:  grur1a  8457  grur1  8458  grutsk  8460
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-ac2 8105
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-riota 6320  df-recs 6404  df-1o 6495  df-er 6676  df-map 6790  df-en 6880  df-dom 6881  df-sdom 6882  df-card 7588  df-cf 7590  df-ac 7759  df-ina 8323  df-gru 8429
  Copyright terms: Public domain W3C validator