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 e. No <-> E. x e. On A : x --> { 1o , 2o } )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. No -> A e. _V )
2		fex	|- ( ( A : x --> { 1o , 2o } /\ x e. On ) -> A e. _V )
3	2	ancoms	|- ( ( x e. On /\ A : x --> { 1o , 2o } ) -> A e. _V )
4	3	rexlimiva	|- ( E. x e. On A : x --> { 1o , 2o } -> A e. _V )
5		feq1	|- ( f = A -> ( f : x --> { 1o , 2o } <-> A : x --> { 1o , 2o } ) )
6	5	rexbidv	|- ( f = A -> ( E. x e. On f : x --> { 1o , 2o } <-> E. x e. On A : x --> { 1o , 2o } ) )
7		df-no	|- No = { f | E. x e. On f : x --> { 1o , 2o } }
8	6 7	elab2g	|- ( A e. _V -> ( A e. No <-> E. x e. On A : x --> { 1o , 2o } ) )
9	1 4 8	pm5.21nii	|- ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )