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	|- ( _om e. On \/ _om = On )

Proof

Step	Hyp	Ref	Expression
1		ordom	|- Ord _om
2		ordeleqon	|- ( Ord _om <-> ( _om e. On \/ _om = On ) )
3	1 2	mpbi	|- ( _om e. On \/ _om = On )