Definition df-cuts 27911

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-cuts	⊢ |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-cuts

Step	Hyp	Ref	Expression
1		ccuts 27910	. 2 class |s
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		csur 27762	. . . 4 class No
5	4	cpw 4558	. . 3 class 𝒫 No
6		cslts 27908	. . . 4 class <<s
7	2	cv 1562	. . . . 5 class 𝑎
8	7	csn 4585	. . . 4 class {𝑎}
9	6, 8	cima 5655	. . 3 class ( <<s “ {𝑎})
10		vx	. . . . . . 7 setvar 𝑥
11	10	cv 1562	. . . . . 6 class 𝑥
12		cbday 27764	. . . . . 6 class bday
13	11, 12	cfv 6525	. . . . 5 class ( bday ‘𝑥)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1562	. . . . . . . . . . 11 class 𝑦
16	15	csn 4585	. . . . . . . . . 10 class {𝑦}
17	7, 16, 6	wbr 5105	. . . . . . . . 9 wff 𝑎 <<s {𝑦}
18	3	cv 1562	. . . . . . . . . 10 class 𝑏
19	16, 18, 6	wbr 5105	. . . . . . . . 9 wff {𝑦} <<s 𝑏
20	17, 19	wa 400	. . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
21	20, 14, 4	crab 3417	. . . . . . 7 class {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
22	12, 21	cima 5655	. . . . . 6 class ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
23	22	cint 4908	. . . . 5 class ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
24	13, 23	wceq 1563	. . . 4 wff ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
25	24, 10, 21	crio 7356	. . 3 class (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
26	2, 3, 5, 9, 25	cmpo 7402	. 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
27	1, 26	wceq 1563	1 wff |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

This definition is referenced by:  cutsval  27931  dmcuts  27942  cutsf  27943