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)