Theorem elreno

Description: Membership in the set of surreal reals. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	elreno	|- ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( y = A -> ( ( -us ` n ) ( -us ` n )
2		breq1	|- ( y = A -> ( y A
3	1 2	anbi12d	|- ( y = A -> ( ( ( -us ` n ) ( ( -us ` n )
4	3	rexbidv	|- ( y = A -> ( E. n e. NN_s ( ( -us ` n ) E. n e. NN_s ( ( -us ` n )
5		id	|- ( y = A -> y = A )
6		oveq1	|- ( y = A -> ( y -s ( 1s /su n ) ) = ( A -s ( 1s /su n ) ) )
7	6	eqeq2d	|- ( y = A -> ( x = ( y -s ( 1s /su n ) ) <-> x = ( A -s ( 1s /su n ) ) ) )
8	7	rexbidv	|- ( y = A -> ( E. n e. NN_s x = ( y -s ( 1s /su n ) ) <-> E. n e. NN_s x = ( A -s ( 1s /su n ) ) ) )
9	8	abbidv	|- ( y = A -> { x | E. n e. NN_s x = ( y -s ( 1s /su n ) ) } = { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } )
10		oveq1	|- ( y = A -> ( y +s ( 1s /su n ) ) = ( A +s ( 1s /su n ) ) )
11	10	eqeq2d	|- ( y = A -> ( x = ( y +s ( 1s /su n ) ) <-> x = ( A +s ( 1s /su n ) ) ) )
12	11	rexbidv	|- ( y = A -> ( E. n e. NN_s x = ( y +s ( 1s /su n ) ) <-> E. n e. NN_s x = ( A +s ( 1s /su n ) ) ) )
13	12	abbidv	|- ( y = A -> { x | E. n e. NN_s x = ( y +s ( 1s /su n ) ) } = { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } )
14	9 13	oveq12d	|- ( y = A -> ( { x | E. n e. NN_s x = ( y -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( y +s ( 1s /su n ) ) } ) = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) )
15	5 14	eqeq12d	|- ( y = A -> ( y = ( { x | E. n e. NN_s x = ( y -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( y +s ( 1s /su n ) ) } ) <-> A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) ) )
16	4 15	anbi12d	|- ( y = A -> ( ( E. n e. NN_s ( ( -us ` n ) ( E. n e. NN_s ( ( -us ` n )
17		df-reno	|- RR_s = { y e. No | ( E. n e. NN_s ( ( -us ` n )
18	16 17	elrab2	|- ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )