Theorem elno

Description: Membership in the surreals. (Contributed by Scott Fenton, 11-Jun-2011) (Proof shortened by SF, 14-Apr-2012) Avoid ax-rep . (Revised by SN, 5-Jun-2025)

	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		vex	|- x e. _V
3		prex	|- { 1o , 2o } e. _V
4		fex2	|- ( ( A : x --> { 1o , 2o } /\ x e. _V /\ { 1o , 2o } e. _V ) -> A e. _V )
5	2 3 4	mp3an23	|- ( A : x --> { 1o , 2o } -> A e. _V )
6	5	rexlimivw	|- ( E. x e. On A : x --> { 1o , 2o } -> A e. _V )
7		feq1	|- ( f = A -> ( f : x --> { 1o , 2o } <-> A : x --> { 1o , 2o } ) )
8	7	rexbidv	|- ( f = A -> ( E. x e. On f : x --> { 1o , 2o } <-> E. x e. On A : x --> { 1o , 2o } ) )
9		df-no	|- No = { f | E. x e. On f : x --> { 1o , 2o } }
10	8 9	elab2g	|- ( A e. _V -> ( A e. No <-> E. x e. On A : x --> { 1o , 2o } ) )
11	1 6 10	pm5.21nii	|- ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )