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 ω ) ) ≠ ( ℵ ‘ ω )

Proof

Step	Hyp	Ref	Expression
1		sdomirr	⊢ ¬ ω ≺ ω
2		2onn	⊢ 2o ∈ ω
3	2	elexi	⊢ 2o ∈ V
4		domrefg	⊢ ( 2o ∈ V → 2o ≼ 2o )
5	3	cfpwsdom	⊢ ( 2o ≼ 2o → ( ℵ ‘ ∅ ) ≺ ( cf ‘ ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) ) )
6	3 4 5	mp2b	⊢ ( ℵ ‘ ∅ ) ≺ ( cf ‘ ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) )
7		aleph0	⊢ ( ℵ ‘ ∅ ) = ω
8	7	a1i	⊢ ( ( card ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) → ( ℵ ‘ ∅ ) = ω )
9	7	oveq2i	⊢ ( 2o ↑m ( ℵ ‘ ∅ ) ) = ( 2o ↑m ω )
10	9	fveq2i	⊢ ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) = ( card ‘ ( 2o ↑m ω ) )
11	10	eqeq1i	⊢ ( ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) = ( ℵ ‘ ω ) ↔ ( card ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) )
12	11	biimpri	⊢ ( ( card ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) → ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) = ( ℵ ‘ ω ) )
13	12	fveq2d	⊢ ( ( card ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) → ( cf ‘ ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) ) = ( 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 ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) → ( cf ‘ ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) ) = ω )
20	8 19	breq12d	⊢ ( ( card ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) → ( ( ℵ ‘ ∅ ) ≺ ( cf ‘ ( card ‘ ( 2o ↑m ( ℵ ‘ ∅ ) ) ) ) ↔ ω ≺ ω ) )
21	6 20	mpbii	⊢ ( ( card ‘ ( 2o ↑m ω ) ) = ( ℵ ‘ ω ) → ω ≺ ω )
22	21	necon3bi	⊢ ( ¬ ω ≺ ω → ( card ‘ ( 2o ↑m ω ) ) ≠ ( ℵ ‘ ω ) )
23	1 22	ax-mp	⊢ ( card ‘ ( 2o ↑m ω ) ) ≠ ( ℵ ‘ ω )