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 syl6eq ⊢ ( 𝑥 = ∅ → ( ℵ ‘ 𝑥 ) = ω )
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 𝑥 ) )