Theorem nodmon

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

	Ref	Expression
Assertion	nodmon	|- ( A e. No -> dom A e. On )

Proof

Step	Hyp	Ref	Expression
1		elno	|- ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )
2		fdm	|- ( A : x --> { 1o , 2o } -> dom A = x )
3	2	eleq1d	|- ( A : x --> { 1o , 2o } -> ( dom A e. On <-> x e. On ) )
4	3	biimprcd	|- ( x e. On -> ( A : x --> { 1o , 2o } -> dom A e. On ) )
5	4	rexlimiv	|- ( E. x e. On A : x --> { 1o , 2o } -> dom A e. On )
6	1 5	sylbi	|- ( A e. No -> dom A e. On )