Definition df-reno 28426

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.)

Assertion

Ref	Expression
df-reno	⊢ ℝs = {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}

Distinct variable group:   𝑥,𝑦,𝑛

Detailed syntax breakdown of Definition df-reno

Step	Hyp	Ref	Expression
1		creno 28425	. 2 class ℝs
2		vn	. . . . . . . . 9 setvar 𝑛
3	2	cv 1539	. . . . . . . 8 class 𝑛
4		cnegs 28051	. . . . . . . 8 class -us
5	3, 4	cfv 6561	. . . . . . 7 class ( -us ‘𝑛)
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1539	. . . . . . 7 class 𝑥
8		cslt 27685	. . . . . . 7 class <s
9	5, 7, 8	wbr 5143	. . . . . 6 wff ( -us ‘𝑛) <s 𝑥
10	7, 3, 8	wbr 5143	. . . . . 6 wff 𝑥 <s 𝑛
11	9, 10	wa 395	. . . . 5 wff (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛)
12		cnns 28319	. . . . 5 class ℕs
13	11, 2, 12	wrex 3070	. . . 4 wff ∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛)
14		vy	. . . . . . . . . 10 setvar 𝑦
15	14	cv 1539	. . . . . . . . 9 class 𝑦
16		c1s 27868	. . . . . . . . . . 11 class 1s
17		cdivs 28213	. . . . . . . . . . 11 class /su
18	16, 3, 17	co 7431	. . . . . . . . . 10 class ( 1s /su 𝑛)
19		csubs 28052	. . . . . . . . . 10 class -s
20	7, 18, 19	co 7431	. . . . . . . . 9 class (𝑥 -s ( 1s /su 𝑛))
21	15, 20	wceq 1540	. . . . . . . 8 wff 𝑦 = (𝑥 -s ( 1s /su 𝑛))
22	21, 2, 12	wrex 3070	. . . . . . 7 wff ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))
23	22, 14	cab 2714	. . . . . 6 class {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))}
24		cadds 27992	. . . . . . . . . 10 class +s
25	7, 18, 24	co 7431	. . . . . . . . 9 class (𝑥 +s ( 1s /su 𝑛))
26	15, 25	wceq 1540	. . . . . . . 8 wff 𝑦 = (𝑥 +s ( 1s /su 𝑛))
27	26, 2, 12	wrex 3070	. . . . . . 7 wff ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))
28	27, 14	cab 2714	. . . . . 6 class {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}
29		cscut 27827	. . . . . 6 class |s
30	23, 28, 29	co 7431	. . . . 5 class ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))})
31	7, 30	wceq 1540	. . . 4 wff 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))})
32	13, 31	wa 395	. . 3 wff (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))
33		csur 27684	. . 3 class No
34	32, 6, 33	crab 3436	. 2 class {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}
35	1, 34	wceq 1540	1 wff ℝs = {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}

This definition is referenced by:  elreno  28427