Metamath Proof Explorer


Definition df-divs

Description: Define surreal division. This is not the definition used in the literature, but we use it here because it is technically easier to work with. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion df-divs / su = x No , y No 0 s ι z No | y s z = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdivs class / su
1 vx setvar x
2 csur class No
3 vy setvar y
4 c0s class 0 s
5 4 csn class 0 s
6 2 5 cdif class No 0 s
7 vz setvar z
8 3 cv setvar y
9 cmuls class s
10 7 cv setvar z
11 8 10 9 co class y s z
12 1 cv setvar x
13 11 12 wceq wff y s z = x
14 13 7 2 crio class ι z No | y s z = x
15 1 3 2 6 14 cmpo class x No , y No 0 s ι z No | y s z = x
16 0 15 wceq wff / su = x No , y No 0 s ι z No | y s z = x