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 e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdivs	|- /su
1		vx	|- x
2		csur	|- No
3		vy	|- y
4		c0s	|- 0s
5	4	csn	|- { 0s }
6	2 5	cdif	|- ( No \ { 0s } )
7		vz	|- z
8	3	cv	|- y
9		cmuls	|- x.s
10	7	cv	|- z
11	8 10 9	co	|- ( y x.s z )
12	1	cv	|- x
13	11 12	wceq	|- ( y x.s z ) = x
14	13 7 2	crio	|- ( iota_ z e. No ( y x.s z ) = x )
15	1 3 2 6 14	cmpo	|- ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) )
16	0 15	wceq	|- /su = ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) )