This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephom

Description: From canth2 , we know that ( aleph0 ) < ( 2 ^om ) , but we cannot prove that ( 2 ^ om ) = ( aleph1 ) (this is the Continuum Hypothesis), nor can we prove that it is less than any bound whatsoever (i.e. the statement ( alephA ) < ( 2 ^om ) is consistent for any ordinal A ). However, we can prove that ( 2 ^ om ) is not equal to ( aleph_om ) , nor ( aleph( aleph_om ) ) , on cofinality grounds, because by Konig's Theorem konigth (in the form of cfpwsdom ), ( 2 ^om ) has uncountable cofinality, which eliminates limit alephs like ( alephom ) . (The first limit aleph that is not eliminated is ( aleph( aleph1 ) ) , which has cofinality ( aleph1 ) .) (Contributed by Mario Carneiro, 21-Mar-2013)

Ref Expression
Assertion alephom ⊢ card ⁡ 2 𝑜 ω ≠ ℵ ⁡ ω

Proof

Step Hyp Ref Expression
1 sdomirr ⊢ ¬ ω ≺ ω
2 2onn ⊢ 2 𝑜 ∈ ω
3 2 elexi ⊢ 2 𝑜 ∈ V
4 domrefg ⊢ 2 𝑜 ∈ V → 2 𝑜 ≼ 2 𝑜
5 3 cfpwsdom ⊢ 2 𝑜 ≼ 2 𝑜 → ℵ ⁡ ∅ ≺ cf ⁡ card ⁡ 2 𝑜 ℵ ⁡ ∅
6 3 4 5 mp2b ⊢ ℵ ⁡ ∅ ≺ cf ⁡ card ⁡ 2 𝑜 ℵ ⁡ ∅
7 aleph0 ⊢ ℵ ⁡ ∅ = ω
8 7 a1i ⊢ card ⁡ 2 𝑜 ω = ℵ ⁡ ω → ℵ ⁡ ∅ = ω
9 7 oveq2i ⊢ 2 𝑜 ℵ ⁡ ∅ = 2 𝑜 ω
10 9 fveq2i ⊢ card ⁡ 2 𝑜 ℵ ⁡ ∅ = card ⁡ 2 𝑜 ω
11 10 eqeq1i ⊢ card ⁡ 2 𝑜 ℵ ⁡ ∅ = ℵ ⁡ ω ↔ card ⁡ 2 𝑜 ω = ℵ ⁡ ω
12 11 biimpri ⊢ card ⁡ 2 𝑜 ω = ℵ ⁡ ω → card ⁡ 2 𝑜 ℵ ⁡ ∅ = ℵ ⁡ ω
13 12 fveq2d ⊢ card ⁡ 2 𝑜 ω = ℵ ⁡ ω → cf ⁡ card ⁡ 2 𝑜 ℵ ⁡ ∅ = cf ⁡ ℵ ⁡ ω
14 limom ⊢ Lim ⁡ ω
15 alephsing ⊢ Lim ⁡ ω → cf ⁡ ℵ ⁡ ω = cf ⁡ ω
16 14 15 ax-mp ⊢ cf ⁡ ℵ ⁡ ω = cf ⁡ ω
17 cfom ⊢ cf ⁡ ω = ω
18 16 17 eqtri ⊢ cf ⁡ ℵ ⁡ ω = ω
19 13 18 eqtrdi ⊢ card ⁡ 2 𝑜 ω = ℵ ⁡ ω → cf ⁡ card ⁡ 2 𝑜 ℵ ⁡ ∅ = ω
20 8 19 breq12d ⊢ card ⁡ 2 𝑜 ω = ℵ ⁡ ω → ℵ ⁡ ∅ ≺ cf ⁡ card ⁡ 2 𝑜 ℵ ⁡ ∅ ↔ ω ≺ ω
21 6 20 mpbii ⊢ card ⁡ 2 𝑜 ω = ℵ ⁡ ω → ω ≺ ω
22 21 necon3bi ⊢ ¬ ω ≺ ω → card ⁡ 2 𝑜 ω ≠ ℵ ⁡ ω
23 1 22 ax-mp ⊢ card ⁡ 2 𝑜 ω ≠ ℵ ⁡ ω