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	$$⊢{ℝ}_s=\left\{x\in \mathrm{No}|\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}x\wedge x{<}_{s}n\right)\wedge x=\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creno	$$class{ℝ}_s$$
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vn	$$setvarn$$
4		cnns	$$class{\mathbb{N}}_s$$
5		cnegs	$$class{+}_s$$
6	3	cv	$$setvarn$$
7	6 5	cfv	$$class{+}_s\left(n\right)$$
8		cslt	$$class{<}_s$$
9	1	cv	$$setvarx$$
10	7 9 8	wbr	$$wff{+}_s\left(n\right){<}_{s}x$$
11	9 6 8	wbr	$$wffx{<}_{s}n$$
12	10 11	wa	$$wff\left({+}_s\left(n\right){<}_{s}x\wedge x{<}_{s}n\right)$$
13	12 3 4	wrex	$$wff\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}x\wedge x{<}_{s}n\right)$$
14		vy	$$setvary$$
15	14	cv	$$setvary$$
16		csubs	$$class{-}_s$$
17		c1s	$$class{1}_s$$
18		cdivs	$$class{/}_{\mathrm{su}}$$
19	17 6 18	co	$$class\left(1_s{/}_{\mathrm{su}}n\right)$$
20	9 19 16	co	$$class\left(x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
21	15 20	wceq	$$wffy=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
22	21 3 4	wrex	$$wff\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
23	22 14	cab	$$class\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
24		cscut	$$class{|}_s$$
25		cadds	$$class{+}_s$$
26	9 19 25	co	$$class\left(x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right)$$
27	15 26	wceq	$$wffy=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
28	27 3 4	wrex	$$wff\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)$$
29	28 14	cab	$$class\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
30	23 29 24	co	$$class\left(\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)$$
31	9 30	wceq	$$wffx=\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}$$
32	13 31	wa	$$wff\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}x\wedge x{<}_{s}n\right)\wedge x=\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)$$
33	32 1 2	crab	$$class\left\{x\in \mathrm{No}|\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}x\wedge x{<}_{s}n\right)\wedge x=\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right\}$$
34	0 33	wceq	$$wff{ℝ}_s=\left\{x\in \mathrm{No}|\left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}x\wedge x{<}_{s}n\right)\wedge x=\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{y|\exists n\in {\mathbb{N}}_{s}y=x{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right\}$$