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 ( ( 𝐴 ∈ Inaccw𝐴 ≠ ω ) → ∃ 𝑥 ( ( ℵ ‘ 𝑥 ) = 𝐴 ∧ Lim 𝑥 ) )

Proof

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