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 Inacc 𝑤 A ω x x = A Lim x

Proof

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