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	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)\ne \aleph \left(\mathrm{\omega }\right)$$

Proof

Step	Hyp	Ref	Expression
1		sdomirr	$$⊢\neg \mathrm{\omega }\prec \mathrm{\omega }$$
2		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
3	2	elexi	$$⊢2_{𝑜}\in \mathrm{V}$$
4		domrefg	$$⊢2_{𝑜}\in \mathrm{V}\to 2_{𝑜}\preccurlyeq 2_{𝑜}$$
5	3	cfpwsdom	$$⊢2_{𝑜}\preccurlyeq 2_{𝑜}\to \aleph \left(\varnothing \right)\prec \mathrm{cf}\left(\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\right)$$
6	3 4 5	mp2b	$$⊢\aleph \left(\varnothing \right)\prec \mathrm{cf}\left(\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\right)$$
7		aleph0	$$⊢\aleph \left(\varnothing \right)=\mathrm{\omega }$$
8	7	a1i	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)\to \aleph \left(\varnothing \right)=\mathrm{\omega }$$
9	7	oveq2i	$$⊢{2_{𝑜}}^{\aleph \left(\varnothing \right)}={2_{𝑜}}^{\mathrm{\omega }}$$
10	9	fveq2i	$$⊢\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)=\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)$$
11	10	eqeq1i	$$⊢\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)=\aleph \left(\mathrm{\omega }\right)\leftrightarrow \mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)$$
12	11	biimpri	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)\to \mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)=\aleph \left(\mathrm{\omega }\right)$$
13	12	fveq2d	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)\to \mathrm{cf}\left(\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\right)=\mathrm{cf}\left(\aleph \left(\mathrm{\omega }\right)\right)$$
14		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
15		alephsing	$$⊢\mathrm{Lim}\mathrm{\omega }\to \mathrm{cf}\left(\aleph \left(\mathrm{\omega }\right)\right)=\mathrm{cf}\left(\mathrm{\omega }\right)$$
16	14 15	ax-mp	$$⊢\mathrm{cf}\left(\aleph \left(\mathrm{\omega }\right)\right)=\mathrm{cf}\left(\mathrm{\omega }\right)$$
17		cfom	$$⊢\mathrm{cf}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$
18	16 17	eqtri	$$⊢\mathrm{cf}\left(\aleph \left(\mathrm{\omega }\right)\right)=\mathrm{\omega }$$
19	13 18	eqtrdi	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)\to \mathrm{cf}\left(\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\right)=\mathrm{\omega }$$
20	8 19	breq12d	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)\to \left(\aleph \left(\varnothing \right)\prec \mathrm{cf}\left(\mathrm{card}\left({2_{𝑜}}^{\aleph \left(\varnothing \right)}\right)\right)\leftrightarrow \mathrm{\omega }\prec \mathrm{\omega }\right)$$
21	6 20	mpbii	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)=\aleph \left(\mathrm{\omega }\right)\to \mathrm{\omega }\prec \mathrm{\omega }$$
22	21	necon3bi	$$⊢\neg \mathrm{\omega }\prec \mathrm{\omega }\to \mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)\ne \aleph \left(\mathrm{\omega }\right)$$
23	1 22	ax-mp	$$⊢\mathrm{card}\left({2_{𝑜}}^{\mathrm{\omega }}\right)\ne \aleph \left(\mathrm{\omega }\right)$$