Theorem cardom

Description: The set of natural numbers is a cardinal number. Theorem 18.11 of Monk1 p. 133. (Contributed by NM, 28-Oct-2003)

	Ref	Expression
Assertion	cardom	⊢ ( card ‘ ω ) = ω

Proof

Step	Hyp	Ref	Expression
1		omelon	⊢ ω ∈ On
2		oncardid	⊢ ( ω ∈ On → ( card ‘ ω ) ≈ ω )
3	1 2	ax-mp	⊢ ( card ‘ ω ) ≈ ω
4		nnsdom	⊢ ( ( card ‘ ω ) ∈ ω → ( card ‘ ω ) ≺ ω )
5		sdomnen	⊢ ( ( card ‘ ω ) ≺ ω → ¬ ( card ‘ ω ) ≈ ω )
6	4 5	syl	⊢ ( ( card ‘ ω ) ∈ ω → ¬ ( card ‘ ω ) ≈ ω )
7	3 6	mt2	⊢ ¬ ( card ‘ ω ) ∈ ω
8		cardonle	⊢ ( ω ∈ On → ( card ‘ ω ) ⊆ ω )
9	1 8	ax-mp	⊢ ( card ‘ ω ) ⊆ ω
10		cardon	⊢ ( card ‘ ω ) ∈ On
11	10 1	onsseli	⊢ ( ( card ‘ ω ) ⊆ ω ↔ ( ( card ‘ ω ) ∈ ω ∨ ( card ‘ ω ) = ω ) )
12	9 11	mpbi	⊢ ( ( card ‘ ω ) ∈ ω ∨ ( card ‘ ω ) = ω )
13	7 12	mtpor	⊢ ( card ‘ ω ) = ω