Definition df-reno

Description: Define the surreal reals. These are the finite numbers without any infintesimal parts. Definition from Conway p. 24. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	df-reno	|- RR_s = { x e. No | ( E. n e. NN_s ( ( -us ` n )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creno	|- RR_s
1		vx	|- x
2		csur	|- No
3		vn	|- n
4		cnns	|- NN_s
5		cnegs	|- -us
6	3	cv	|- n
7	6 5	cfv	|- ( -us ` n )
8		cslt	|-
9	1	cv	|- x
10	7 9 8	wbr	|- ( -us ` n )
11	9 6 8	wbr	|- x
12	10 11	wa	|- ( ( -us ` n )
13	12 3 4	wrex	|- E. n e. NN_s ( ( -us ` n )
14		vy	|- y
15	14	cv	|- y
16		csubs	|- -s
17		c1s	|- 1s
18		cdivs	|- /su
19	17 6 18	co	|- ( 1s /su n )
20	9 19 16	co	|- ( x -s ( 1s /su n ) )
21	15 20	wceq	|- y = ( x -s ( 1s /su n ) )
22	21 3 4	wrex	|- E. n e. NN_s y = ( x -s ( 1s /su n ) )
23	22 14	cab	|- { y | E. n e. NN_s y = ( x -s ( 1s /su n ) ) }
24		cscut	|- |s
25		cadds	|- +s
26	9 19 25	co	|- ( x +s ( 1s /su n ) )
27	15 26	wceq	|- y = ( x +s ( 1s /su n ) )
28	27 3 4	wrex	|- E. n e. NN_s y = ( x +s ( 1s /su n ) )
29	28 14	cab	|- { y | E. n e. NN_s y = ( x +s ( 1s /su n ) ) }
30	23 29 24	co	|- ( { y | E. n e. NN_s y = ( x -s ( 1s /su n ) ) } |s { y | E. n e. NN_s y = ( x +s ( 1s /su n ) ) } )
31	9 30	wceq	|- x = ( { y | E. n e. NN_s y = ( x -s ( 1s /su n ) ) } |s { y | E. n e. NN_s y = ( x +s ( 1s /su n ) ) } )
32	13 31	wa	|- ( E. n e. NN_s ( ( -us ` n )
33	32 1 2	crab	|- { x e. No | ( E. n e. NN_s ( ( -us ` n )
34	0 33	wceq	|- RR_s = { x e. No | ( E. n e. NN_s ( ( -us ` n )