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 card2𝑜ωω

Proof

Step Hyp Ref Expression
1 sdomirr ¬ωω
2 2onn 2𝑜ω
3 2 elexi 2𝑜V
4 domrefg 2𝑜V2𝑜2𝑜
5 3 cfpwsdom 2𝑜2𝑜cfcard2𝑜
6 3 4 5 mp2b cfcard2𝑜
7 aleph0 =ω
8 7 a1i card2𝑜ω=ω=ω
9 7 oveq2i 2𝑜=2𝑜ω
10 9 fveq2i card2𝑜=card2𝑜ω
11 10 eqeq1i card2𝑜=ωcard2𝑜ω=ω
12 11 biimpri card2𝑜ω=ωcard2𝑜=ω
13 12 fveq2d card2𝑜ω=ωcfcard2𝑜=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 card2𝑜ω=ωcfcard2𝑜=ω
20 8 19 breq12d card2𝑜ω=ωcfcard2𝑜ωω
21 6 20 mpbii card2𝑜ω=ωωω
22 21 necon3bi ¬ωωcard2𝑜ωω
23 1 22 ax-mp card2𝑜ωω