Theorem elno

Description: Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011)

	Ref	Expression
Assertion	elno	$$⊢A\in \mathrm{No}\leftrightarrow \exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \mathrm{No}\to A\in \mathrm{V}$$
2		fex	$$⊢\left(A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\wedge x\in \mathrm{On}\right)\to A\in \mathrm{V}$$
3	2	ancoms	$$⊢\left(x\in \mathrm{On}\wedge A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\right)\to A\in \mathrm{V}$$
4	3	rexlimiva	$$⊢\exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\to A\in \mathrm{V}$$
5		feq1	$$⊢f=A\to \left(f:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\leftrightarrow A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\right)$$
6	5	rexbidv	$$⊢f=A\to \left(\exists x\in \mathrm{On}f:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\leftrightarrow \exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\right)$$
7		df-no	$$⊢\mathrm{No}=\left\{f|\exists x\in \mathrm{On}f:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\right\}$$
8	6 7	elab2g	$$⊢A\in \mathrm{V}\to \left(A\in \mathrm{No}\leftrightarrow \exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\right)$$
9	1 4 8	pm5.21nii	$$⊢A\in \mathrm{No}\leftrightarrow \exists x\in \mathrm{On}A:x⟶\left\{1_{𝑜},2_{𝑜}\right\}$$