Metamath Proof Explorer

Theorem nodmord

Description: The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011)

		Ref	Expression
	Assertion	nodmord	$⊢ A \in No \to Ord dom A$

Step	Hyp	Ref	Expression
1		nodmon	$⊢ A \in No \to dom A \in On$
2		eloni	$⊢ dom A \in On \to Ord dom A$
3	1 2	syl	$⊢ A \in No \to Ord dom A$