Theorem cfom

Description: Value of the cofinality function at omega (the set of natural numbers). Exercise 4 of TakeutiZaring p. 102. (Contributed by NM, 23-Apr-2004) (Proof shortened by Mario Carneiro, 11-Jun-2015)

	Ref	Expression
Assertion	cfom	$$⊢\mathrm{cf}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		cfle	$$⊢\mathrm{cf}\left(\mathrm{\omega }\right)\subseteq \mathrm{\omega }$$
2		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
3		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
4	3	cflim2	$$⊢\mathrm{Lim}\mathrm{\omega }\leftrightarrow \mathrm{Lim}\mathrm{cf}\left(\mathrm{\omega }\right)$$
5	2 4	mpbi	$$⊢\mathrm{Lim}\mathrm{cf}\left(\mathrm{\omega }\right)$$
6		limomss	$$⊢\mathrm{Lim}\mathrm{cf}\left(\mathrm{\omega }\right)\to \mathrm{\omega }\subseteq \mathrm{cf}\left(\mathrm{\omega }\right)$$
7	5 6	ax-mp	$$⊢\mathrm{\omega }\subseteq \mathrm{cf}\left(\mathrm{\omega }\right)$$
8	1 7	eqssi	$$⊢\mathrm{cf}\left(\mathrm{\omega }\right)=\mathrm{\omega }$$