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	Could not format assertion : No typesetting found for |- /su = ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdivs	Could not format /su : No typesetting found for class /su with typecode class
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vy	$$setvary$$
4		c0s	Could not format 0s : No typesetting found for class 0s with typecode class
5	4	csn	Could not format { 0s } : No typesetting found for class { 0s } with typecode class
6	2 5	cdif	Could not format ( No \ { 0s } ) : No typesetting found for class ( No \ { 0s } ) with typecode class
7		vz	$$setvarz$$
8	3	cv	$$setvary$$
9		cmuls	Could not format x.s : No typesetting found for class x.s with typecode class
10	7	cv	$$setvarz$$
11	8 10 9	co	Could not format ( y x.s z ) : No typesetting found for class ( y x.s z ) with typecode class
12	1	cv	$$setvarx$$
13	11 12	wceq	Could not format ( y x.s z ) = x : No typesetting found for wff ( y x.s z ) = x with typecode wff
14	13 7 2	crio	Could not format ( iota_ z e. No ( y x.s z ) = x ) : No typesetting found for class ( iota_ z e. No ( y x.s z ) = x ) with typecode class
15	1 3 2 6 14	cmpo	Could not format ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) ) : No typesetting found for class ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) ) with typecode class
16	0 15	wceq	Could not format /su = ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) ) : No typesetting found for wff /su = ( x e. No , y e. ( No \ { 0s } ) |-> ( iota_ z e. No ( y x.s z ) = x ) ) with typecode wff