Theorem norn

Description: The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	norn	$$⊢A\in \mathrm{No}\to \mathrm{ran}A\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elno	$$⊢A\in \mathrm{No}\leftrightarrow \exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}$$
2		frn	$$⊢A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to \mathrm{ran}A\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$
3	2	rexlimivw	$$⊢\exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to \mathrm{ran}A\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$
4	1 3	sylbi	$$⊢A\in \mathrm{No}\to \mathrm{ran}A\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$