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 ` ( 2o ^m _om ) ) =/= ( aleph ` _om )

Proof

Step Hyp Ref Expression
1 sdomirr 
 |-  -. _om ~< _om
2 2onn 
 |-  2o e. _om
3 2 elexi 
 |-  2o e. _V
4 domrefg 
 |-  ( 2o e. _V -> 2o ~<_ 2o )
5 3 cfpwsdom 
 |-  ( 2o ~<_ 2o -> ( aleph ` (/) ) ~< ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) )
6 3 4 5 mp2b 
 |-  ( aleph ` (/) ) ~< ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) )
7 aleph0 
 |-  ( aleph ` (/) ) = _om
8 7 a1i 
 |-  ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( aleph ` (/) ) = _om )
9 7 oveq2i 
 |-  ( 2o ^m ( aleph ` (/) ) ) = ( 2o ^m _om )
10 9 fveq2i 
 |-  ( card ` ( 2o ^m ( aleph ` (/) ) ) ) = ( card ` ( 2o ^m _om ) )
11 10 eqeq1i 
 |-  ( ( card ` ( 2o ^m ( aleph ` (/) ) ) ) = ( aleph ` _om ) <-> ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) )
12 11 biimpri 
 |-  ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( card ` ( 2o ^m ( aleph ` (/) ) ) ) = ( aleph ` _om ) )
13 12 fveq2d 
 |-  ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) = ( cf ` ( aleph ` _om ) ) )
14 limom 
 |-  Lim _om
15 alephsing 
 |-  ( Lim _om -> ( cf ` ( aleph ` _om ) ) = ( cf ` _om ) )
16 14 15 ax-mp 
 |-  ( cf ` ( aleph ` _om ) ) = ( cf ` _om )
17 cfom 
 |-  ( cf ` _om ) = _om
18 16 17 eqtri 
 |-  ( cf ` ( aleph ` _om ) ) = _om
19 13 18 eqtrdi 
 |-  ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) = _om )
20 8 19 breq12d 
 |-  ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> ( ( aleph ` (/) ) ~< ( cf ` ( card ` ( 2o ^m ( aleph ` (/) ) ) ) ) <-> _om ~< _om ) )
21 6 20 mpbii 
 |-  ( ( card ` ( 2o ^m _om ) ) = ( aleph ` _om ) -> _om ~< _om )
22 21 necon3bi 
 |-  ( -. _om ~< _om -> ( card ` ( 2o ^m _om ) ) =/= ( aleph ` _om ) )
23 1 22 ax-mp 
 |-  ( card ` ( 2o ^m _om ) ) =/= ( aleph ` _om )