Definition df-subs

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubs	⊢ -s
1		vx	⊢ 𝑥
2		csur	⊢ No
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		cadds	⊢ +s
6		cnegs	⊢ -us
7	3	cv	⊢ 𝑦
8	7 6	cfv	⊢ ( -us ‘ 𝑦 )
9	4 8 5	co	⊢ ( 𝑥 +s ( -us ‘ 𝑦 ) )
10	1 3 2 2 9	cmpo	⊢ ( 𝑥 ∈ No , 𝑦 ∈ No ↦ ( 𝑥 +s ( -us ‘ 𝑦 ) ) )
11	0 10	wceq	⊢ -s = ( 𝑥 ∈ No , 𝑦 ∈ No ↦ ( 𝑥 +s ( -us ‘ 𝑦 ) ) )