Theorem nofun

Description: A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	nofun	$$⊢A\in \mathrm{No}\to \mathrm{Fun}A$$

Proof

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