Metamath Proof Explorer

Definition df-subs

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

Ref Expression
Assertion df-subs 
|- -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubs 
 |-  -s
1 vx 
 |-  x
2 csur 
 |-  No
3 vy 
 |-  y
4 1 cv 
 |-  x
5 cadds 
 |-  +s
6 cnegs 
 |-  -us
7 3 cv 
 |-  y
8 7 6 cfv 
 |-  ( -us ` y )
9 4 8 5 co 
 |-  ( x +s ( -us ` y ) )
10 1 3 2 2 9 cmpo 
 |-  ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) )
11 0 10 wceq 
 |-  -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) )