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

Metamath Proof Explorer

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