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 = ( 𝑥 ∈ No , 𝑦 ∈ ( No ∖ { 0s } ) ↦ ( ℩ 𝑧 ∈ No ( 𝑦 ·s 𝑧 ) = 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdivs	⊢ /su
1		vx	⊢ 𝑥
2		csur	⊢ No
3		vy	⊢ 𝑦
4		c0s	⊢ 0s
5	4	csn	⊢ { 0s }
6	2 5	cdif	⊢ ( No ∖ { 0s } )
7		vz	⊢ 𝑧
8	3	cv	⊢ 𝑦
9		cmuls	⊢ ·s
10	7	cv	⊢ 𝑧
11	8 10 9	co	⊢ ( 𝑦 ·s 𝑧 )
12	1	cv	⊢ 𝑥
13	11 12	wceq	⊢ ( 𝑦 ·s 𝑧 ) = 𝑥
14	13 7 2	crio	⊢ ( ℩ 𝑧 ∈ No ( 𝑦 ·s 𝑧 ) = 𝑥 )
15	1 3 2 6 14	cmpo	⊢ ( 𝑥 ∈ No , 𝑦 ∈ ( No ∖ { 0s } ) ↦ ( ℩ 𝑧 ∈ No ( 𝑦 ·s 𝑧 ) = 𝑥 ) )
16	0 15	wceq	⊢ /su = ( 𝑥 ∈ No , 𝑦 ∈ ( No ∖ { 0s } ) ↦ ( ℩ 𝑧 ∈ No ( 𝑦 ·s 𝑧 ) = 𝑥 ) )