Definition df-scut

Description: Define the cut operator on surreal numbers. This operator, which Conway takes as the primitive operator over surreals, picks the surreal lying between two sets of surreals of minimal birthday. Definition from Gonshor p. 7. (Contributed by Scott Fenton, 7-Dec-2021)

	Ref	Expression
Assertion	df-scut	⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscut	⊢ |s
1		va	⊢ 𝑎
2		csur	⊢ No
3	2	cpw	⊢ 𝒫 No
4		vb	⊢ 𝑏
5		csslt	⊢ <<s
6	1	cv	⊢ 𝑎
7	6	csn	⊢ { 𝑎 }
8	5 7	cima	⊢ ( <<s “ { 𝑎 } )
9		vx	⊢ 𝑥
10		vy	⊢ 𝑦
11	10	cv	⊢ 𝑦
12	11	csn	⊢ { 𝑦 }
13	6 12 5	wbr	⊢ 𝑎 <<s { 𝑦 }
14	4	cv	⊢ 𝑏
15	12 14 5	wbr	⊢ { 𝑦 } <<s 𝑏
16	13 15	wa	⊢ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 )
17	16 10 2	crab	⊢ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) }
18		cbday	⊢ bday
19	9	cv	⊢ 𝑥
20	19 18	cfv	⊢ ( bday ‘ 𝑥 )
21	18 17	cima	⊢ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } )
22	21	cint	⊢ ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } )
23	20 22	wceq	⊢ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } )
24	23 9 17	crio	⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) )
25	1 4 3 8 24	cmpo	⊢ ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
26	0 25	wceq	⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )