Metamath Proof Explorer


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 𝑏 ) } ) ) )