Definition df-subs 28438

Description: Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.)

Assertion

Ref	Expression
df-subs	⊢ −s = (𝑥 ∈ No, 𝑦 ∈ No ↦ (𝑥 +s ( -s‘𝑦)))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-subs

Step	Hyp	Ref	Expression
1		csubs 28436	. 2 class −s
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		csur 28027	. . 3 class No
5	2	cv 1569	. . . 4 class 𝑥
6	3	cv 1569	. . . . 5 class 𝑦
7		cnegs 28435	. . . . 5 class -s
8	6, 7	cfv 6558	. . . 4 class ( -s‘𝑦)
9		cadds 28375	. . . 4 class +s
10	5, 8, 9	co 7443	. . 3 class (𝑥 +s ( -s‘𝑦))
11	2, 3, 4, 4, 10	cmpo 7445	. 2 class (𝑥 ∈ No, 𝑦 ∈ No ↦ (𝑥 +s ( -s‘𝑦)))
12	1, 11	wceq 1570	1 wff −s = (𝑥 ∈ No, 𝑦 ∈ No ↦ (𝑥 +s ( -s‘𝑦)))

This definition is used by:  subsfn  28440  subsval  28476  subsf  28480