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

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 )