Definition df-cuts 27773

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 27772	. 2 class |s
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		csur 27624	. . . 4 class No
5	4	cpw 4556	. . 3 class 𝒫 No
6		cslts 27770	. . . 4 class <<s
7	2	cv 1541	. . . . 5 class 𝑎
8	7	csn 4582	. . . 4 class {𝑎}
9	6, 8	cima 5637	. . 3 class ( <<s “ {𝑎})
10		vx	. . . . . . 7 setvar 𝑥
11	10	cv 1541	. . . . . 6 class 𝑥
12		cbday 27626	. . . . . 6 class bday
13	11, 12	cfv 6502	. . . . 5 class ( bday ‘𝑥)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1541	. . . . . . . . . . 11 class 𝑦
16	15	csn 4582	. . . . . . . . . 10 class {𝑦}
17	7, 16, 6	wbr 5100	. . . . . . . . 9 wff 𝑎 <<s {𝑦}
18	3	cv 1541	. . . . . . . . . 10 class 𝑏
19	16, 18, 6	wbr 5100	. . . . . . . . 9 wff {𝑦} <<s 𝑏
20	17, 19	wa 395	. . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
21	20, 14, 4	crab 3401	. . . . . . 7 class {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
22	12, 21	cima 5637	. . . . . 6 class ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
23	22	cint 4904	. . . . 5 class ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
24	13, 23	wceq 1542	. . . 4 wff ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
25	24, 10, 21	crio 7326	. . 3 class (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
26	2, 3, 5, 9, 25	cmpo 7372	. 2 class (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
27	1, 26	wceq 1542	1 wff |s = (𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

This definition is referenced by:  cutsval  27793  dmcuts  27804  cutsf  27805