Theorem nodmon

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

	Ref	Expression
Assertion	nodmon	$$⊢A\in \mathrm{No}\to \mathrm{dom}A\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		elno	$$⊢A\in \mathrm{No}\leftrightarrow \exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}$$
2		fdm	$$⊢A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to \mathrm{dom}A=x$$
3	2	eleq1d	$$⊢A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to \left(\mathrm{dom}A\in \mathrm{On}\leftrightarrow x\in \mathrm{On}\right)$$
4	3	biimprcd	$$⊢x\in \mathrm{On}\to \left(A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to \mathrm{dom}A\in \mathrm{On}\right)$$
5	4	rexlimiv	$$⊢\exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to \mathrm{dom}A\in \mathrm{On}$$
6	1 5	sylbi	$$⊢A\in \mathrm{No}\to \mathrm{dom}A\in \mathrm{On}$$