Metamath Proof Explorer

Theorem winalim2

Description: A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014)

Ref Expression
Assertion winalim2 
|- ( ( A e. InaccW /\ A =/= _om ) -> E. x ( ( aleph ` x ) = A /\ Lim x ) )

Proof

Step Hyp Ref Expression
1 winacard 
 |-  ( A e. InaccW -> ( card ` A ) = A )
2 winainf 
 |-  ( A e. InaccW -> _om C_ A )
3 cardalephex 
 |-  ( _om C_ A -> ( ( card ` A ) = A <-> E. x e. On A = ( aleph ` x ) ) )
4 2 3 syl 
 |-  ( A e. InaccW -> ( ( card ` A ) = A <-> E. x e. On A = ( aleph ` x ) ) )
5 1 4 mpbid 
 |-  ( A e. InaccW -> E. x e. On A = ( aleph ` x ) )
6 5 adantr 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> E. x e. On A = ( aleph ` x ) )
7 df-rex 
 |-  ( E. x e. On A = ( aleph ` x ) <-> E. x ( x e. On /\ A = ( aleph ` x ) ) )
8 simprr 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> A = ( aleph ` x ) )
9 8 eqcomd 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( aleph ` x ) = A )
10 simprl 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> x e. On )
11 onzsl 
 |-  ( x e. On <-> ( x = (/) \/ E. y e. On x = suc y \/ ( x e. _V /\ Lim x ) ) )
12 10 11 sylib 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( x = (/) \/ E. y e. On x = suc y \/ ( x e. _V /\ Lim x ) ) )
13 simplr 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> A =/= _om )
14 fveq2 
 |-  ( x = (/) -> ( aleph ` x ) = ( aleph ` (/) ) )
15 aleph0 
 |-  ( aleph ` (/) ) = _om
16 14 15 eqtrdi 
 |-  ( x = (/) -> ( aleph ` x ) = _om )
17 eqtr 
 |-  ( ( A = ( aleph ` x ) /\ ( aleph ` x ) = _om ) -> A = _om )
18 16 17 sylan2 
 |-  ( ( A = ( aleph ` x ) /\ x = (/) ) -> A = _om )
19 18 ex 
 |-  ( A = ( aleph ` x ) -> ( x = (/) -> A = _om ) )
20 19 necon3ad 
 |-  ( A = ( aleph ` x ) -> ( A =/= _om -> -. x = (/) ) )
21 8 13 20 sylc 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> -. x = (/) )
22 21 pm2.21d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( x = (/) -> Lim x ) )
23 breq1 
 |-  ( z = ( aleph ` y ) -> ( z ~< w <-> ( aleph ` y ) ~< w ) )
24 23 rexbidv 
 |-  ( z = ( aleph ` y ) -> ( E. w e. A z ~< w <-> E. w e. A ( aleph ` y ) ~< w ) )
25 elwina 
 |-  ( A e. InaccW <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. z e. A E. w e. A z ~< w ) )
26 25 simp3bi 
 |-  ( A e. InaccW -> A. z e. A E. w e. A z ~< w )
27 26 ad3antrrr 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> A. z e. A E. w e. A z ~< w )
28 suceloni 
 |-  ( y e. On -> suc y e. On )
29 vex 
 |-  y e. _V
30 29 sucid 
 |-  y e. suc y
31 alephord2i 
 |-  ( suc y e. On -> ( y e. suc y -> ( aleph ` y ) e. ( aleph ` suc y ) ) )
32 28 30 31 mpisyl 
 |-  ( y e. On -> ( aleph ` y ) e. ( aleph ` suc y ) )
33 32 ad2antrl 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( aleph ` y ) e. ( aleph ` suc y ) )
34 simplrr 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> A = ( aleph ` x ) )
35 fveq2 
 |-  ( x = suc y -> ( aleph ` x ) = ( aleph ` suc y ) )
36 35 ad2antll 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( aleph ` x ) = ( aleph ` suc y ) )
37 34 36 eqtrd 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> A = ( aleph ` suc y ) )
38 33 37 eleqtrrd 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( aleph ` y ) e. A )
39 24 27 38 rspcdva 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> E. w e. A ( aleph ` y ) ~< w )
40 39 expr 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ y e. On ) -> ( x = suc y -> E. w e. A ( aleph ` y ) ~< w ) )
41 iscard 
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. w e. A w ~< A ) )
42 41 simprbi 
 |-  ( ( card ` A ) = A -> A. w e. A w ~< A )
43 rsp 
 |-  ( A. w e. A w ~< A -> ( w e. A -> w ~< A ) )
44 1 42 43 3syl 
 |-  ( A e. InaccW -> ( w e. A -> w ~< A ) )
45 44 ad3antrrr 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( w e. A -> w ~< A ) )
46 37 breq2d 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( w ~< A <-> w ~< ( aleph ` suc y ) ) )
47 45 46 sylibd 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( w e. A -> w ~< ( aleph ` suc y ) ) )
48 alephnbtwn2 
 |-  -. ( ( aleph ` y ) ~< w /\ w ~< ( aleph ` suc y ) )
49 pm3.21 
 |-  ( w ~< ( aleph ` suc y ) -> ( ( aleph ` y ) ~< w -> ( ( aleph ` y ) ~< w /\ w ~< ( aleph ` suc y ) ) ) )
50 48 49 mtoi 
 |-  ( w ~< ( aleph ` suc y ) -> -. ( aleph ` y ) ~< w )
51 47 50 syl6 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> ( w e. A -> -. ( aleph ` y ) ~< w ) )
52 51 imp 
 |-  ( ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) /\ w e. A ) -> -. ( aleph ` y ) ~< w )
53 52 nrexdv 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ ( y e. On /\ x = suc y ) ) -> -. E. w e. A ( aleph ` y ) ~< w )
54 53 expr 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ y e. On ) -> ( x = suc y -> -. E. w e. A ( aleph ` y ) ~< w ) )
55 40 54 pm2.65d 
 |-  ( ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) /\ y e. On ) -> -. x = suc y )
56 55 nrexdv 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> -. E. y e. On x = suc y )
57 56 pm2.21d 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( E. y e. On x = suc y -> Lim x ) )
58 simpr 
 |-  ( ( x e. _V /\ Lim x ) -> Lim x )
59 58 a1i 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( ( x e. _V /\ Lim x ) -> Lim x ) )
60 22 57 59 3jaod 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( ( x = (/) \/ E. y e. On x = suc y \/ ( x e. _V /\ Lim x ) ) -> Lim x ) )
61 12 60 mpd 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> Lim x )
62 9 61 jca 
 |-  ( ( ( A e. InaccW /\ A =/= _om ) /\ ( x e. On /\ A = ( aleph ` x ) ) ) -> ( ( aleph ` x ) = A /\ Lim x ) )
63 62 ex 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> ( ( x e. On /\ A = ( aleph ` x ) ) -> ( ( aleph ` x ) = A /\ Lim x ) ) )
64 63 eximdv 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> ( E. x ( x e. On /\ A = ( aleph ` x ) ) -> E. x ( ( aleph ` x ) = A /\ Lim x ) ) )
65 7 64 syl5bi 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> ( E. x e. On A = ( aleph ` x ) -> E. x ( ( aleph ` x ) = A /\ Lim x ) ) )
66 6 65 mpd 
 |-  ( ( A e. InaccW /\ A =/= _om ) -> E. x ( ( aleph ` x ) = A /\ Lim x ) )