This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( cf ‘ ω ) = ω

Proof

Step	Hyp	Ref	Expression
1		cfle	⊢ ( cf ‘ ω ) ⊆ ω
2		limom	⊢ Lim ω
3		omex	⊢ ω ∈ V
4	3	cflim2	⊢ ( Lim ω ↔ Lim ( cf ‘ ω ) )
5	2 4	mpbi	⊢ Lim ( cf ‘ ω )
6		limomss	⊢ ( Lim ( cf ‘ ω ) → ω ⊆ ( cf ‘ ω ) )
7	5 6	ax-mp	⊢ ω ⊆ ( cf ‘ ω )
8	1 7	eqssi	⊢ ( cf ‘ ω ) = ω