Metamath Proof Explorer


Theorem omon

Description: The class of natural numbers _om is either an ordinal number (if we accept the Axiom of Infinity) or the proper class of all ordinal numbers (if we deny the Axiom of Infinity). Remark in TakeutiZaring p. 43. (Contributed by NM, 10-May-1998)

Ref Expression
Assertion omon ( ω ∈ On ∨ ω = On )

Proof

Step Hyp Ref Expression
1 ordom Ord ω
2 ordeleqon ( Ord ω ↔ ( ω ∈ On ∨ ω = On ) )
3 1 2 mpbi ( ω ∈ On ∨ ω = On )