Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-scut Structured version   Visualization version   GIF version

Definition df-scut 33619
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.)
Assertion
Ref Expression
df-scut |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-scut
StepHypRef Expression
1 cscut 33618 . 2 class |s
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 csur 33484 . . . 4 class No
54cpw 4488 . . 3 class 𝒫 No
6 csslt 33616 . . . 4 class <<s
72cv 1541 . . . . 5 class 𝑎
87csn 4516 . . . 4 class {𝑎}
96, 8cima 5528 . . 3 class ( <<s “ {𝑎})
10 vx . . . . . . 7 setvar 𝑥
1110cv 1541 . . . . . 6 class 𝑥
12 cbday 33486 . . . . . 6 class bday
1311, 12cfv 6339 . . . . 5 class ( bday 𝑥)
14 vy . . . . . . . . . . . 12 setvar 𝑦
1514cv 1541 . . . . . . . . . . 11 class 𝑦
1615csn 4516 . . . . . . . . . 10 class {𝑦}
177, 16, 6wbr 5030 . . . . . . . . 9 wff 𝑎 <<s {𝑦}
183cv 1541 . . . . . . . . . 10 class 𝑏
1916, 18, 6wbr 5030 . . . . . . . . 9 wff {𝑦} <<s 𝑏
2017, 19wa 399 . . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
2120, 14, 4crab 3057 . . . . . . 7 class {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
2212, 21cima 5528 . . . . . 6 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2322cint 4836 . . . . 5 class ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2413, 23wceq 1542 . . . 4 wff ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
2524, 10, 21crio 7126 . . 3 class (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
262, 3, 5, 9, 25cmpo 7172 . 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
271, 26wceq 1542 1 wff |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (𝑥 ∈ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
Colors of variables: wff setvar class
This definition is referenced by:  scutval  33635  dmscut  33646  scutf  33647
  Copyright terms: Public domain W3C validator