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 = { 𝑥 ∈ No ∣ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑥 ∧ 𝑥 <s 𝑛 ) ∧ 𝑥 = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) } ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		creno	⊢ ℝs
1		vx	⊢ 𝑥
2		csur	⊢ No
3		vn	⊢ 𝑛
4		cnns	⊢ ℕs
5		cnegs	⊢ -us
6	3	cv	⊢ 𝑛
7	6 5	cfv	⊢ ( -us ‘ 𝑛 )
8		cslt	⊢ <s
9	1	cv	⊢ 𝑥
10	7 9 8	wbr	⊢ ( -us ‘ 𝑛 ) <s 𝑥
11	9 6 8	wbr	⊢ 𝑥 <s 𝑛
12	10 11	wa	⊢ ( ( -us ‘ 𝑛 ) <s 𝑥 ∧ 𝑥 <s 𝑛 )
13	12 3 4	wrex	⊢ ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑥 ∧ 𝑥 <s 𝑛 )
14		vy	⊢ 𝑦
15	14	cv	⊢ 𝑦
16		csubs	⊢ -s
17		c1s	⊢ 1s
18		cdivs	⊢ /su
19	17 6 18	co	⊢ ( 1s /su 𝑛 )
20	9 19 16	co	⊢ ( 𝑥 -s ( 1s /su 𝑛 ) )
21	15 20	wceq	⊢ 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) )
22	21 3 4	wrex	⊢ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) )
23	22 14	cab	⊢ { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) }
24		cscut	⊢ |s
25		cadds	⊢ +s
26	9 19 25	co	⊢ ( 𝑥 +s ( 1s /su 𝑛 ) )
27	15 26	wceq	⊢ 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) )
28	27 3 4	wrex	⊢ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) )
29	28 14	cab	⊢ { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) }
30	23 29 24	co	⊢ ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) } )
31	9 30	wceq	⊢ 𝑥 = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) } )
32	13 31	wa	⊢ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑥 ∧ 𝑥 <s 𝑛 ) ∧ 𝑥 = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) } ) )
33	32 1 2	crab	⊢ { 𝑥 ∈ No ∣ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑥 ∧ 𝑥 <s 𝑛 ) ∧ 𝑥 = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) } ) ) }
34	0 33	wceq	⊢ ℝs = { 𝑥 ∈ No ∣ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝑥 ∧ 𝑥 <s 𝑛 ) ∧ 𝑥 = ( { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 -s ( 1s /su 𝑛 ) ) } |s { 𝑦 ∣ ∃ 𝑛 ∈ ℕs 𝑦 = ( 𝑥 +s ( 1s /su 𝑛 ) ) } ) ) }