Definition df-reno 28294

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 28293	. 2 class ℝs
2		vn	. . . . . . . . 9 setvar 𝑛
3	2	cv 1532	. . . . . . . 8 class 𝑛
4		cnegs 27978	. . . . . . . 8 class -us
5	3, 4	cfv 6549	. . . . . . 7 class ( -us ‘𝑛)
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1532	. . . . . . 7 class 𝑥
8		cslt 27619	. . . . . . 7 class <s
9	5, 7, 8	wbr 5149	. . . . . 6 wff ( -us ‘𝑛) <s 𝑥
10	7, 3, 8	wbr 5149	. . . . . 6 wff 𝑥 <s 𝑛
11	9, 10	wa 394	. . . . 5 wff (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛)
12		cnns 28236	. . . . 5 class ℕs
13	11, 2, 12	wrex 3059	. . . 4 wff ∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛)
14		vy	. . . . . . . . . 10 setvar 𝑦
15	14	cv 1532	. . . . . . . . 9 class 𝑦
16		c1s 27802	. . . . . . . . . . 11 class 1s
17		cdivs 28137	. . . . . . . . . . 11 class /su
18	16, 3, 17	co 7419	. . . . . . . . . 10 class ( 1s /su 𝑛)
19		csubs 27979	. . . . . . . . . 10 class -s
20	7, 18, 19	co 7419	. . . . . . . . 9 class (𝑥 -s ( 1s /su 𝑛))
21	15, 20	wceq 1533	. . . . . . . 8 wff 𝑦 = (𝑥 -s ( 1s /su 𝑛))
22	21, 2, 12	wrex 3059	. . . . . . 7 wff ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))
23	22, 14	cab 2702	. . . . . 6 class {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))}
24		cadds 27922	. . . . . . . . . 10 class +s
25	7, 18, 24	co 7419	. . . . . . . . 9 class (𝑥 +s ( 1s /su 𝑛))
26	15, 25	wceq 1533	. . . . . . . 8 wff 𝑦 = (𝑥 +s ( 1s /su 𝑛))
27	26, 2, 12	wrex 3059	. . . . . . 7 wff ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))
28	27, 14	cab 2702	. . . . . 6 class {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}
29		cscut 27761	. . . . . 6 class |s
30	23, 28, 29	co 7419	. . . . 5 class ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))})
31	7, 30	wceq 1533	. . . 4 wff 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))})
32	13, 31	wa 394	. . 3 wff (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))
33		csur 27618	. . 3 class No
34	32, 6, 33	crab 3418	. 2 class {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}
35	1, 34	wceq 1533	1 wff ℝs = {𝑥 ∈ No ∣ (∃𝑛 ∈ ℕs (( -us ‘𝑛) <s 𝑥 ∧ 𝑥 <s 𝑛) ∧ 𝑥 = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 -s ( 1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (𝑥 +s ( 1s /su 𝑛))}))}

This definition is referenced by:  elreno  28295