Definition df-cuts 28151

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 28150	. 2 class |s
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		csur 28002	. . . 4 class No
5	4	cpw 4556	. . 3 class 𝒫 No
6		cslts 28148	. . . 4 class <<s
7	2	cv 1568	. . . . 5 class 𝑎
8	7	csn 4584	. . . 4 class {𝑎}
9	6, 8	cima 5653	. . 3 class ( <<s “ {𝑎})
10		vx	. . . . . . 7 setvar 𝑥
11	10	cv 1568	. . . . . 6 class 𝑥
12		cbday 28004	. . . . . 6 class bday
13	11, 12	cfv 6538	. . . . 5 class (bday‘𝑥)
14		vy	. . . . . . . . . . . 12 setvar 𝑦
15	14	cv 1568	. . . . . . . . . . 11 class 𝑦
16	15	csn 4584	. . . . . . . . . 10 class {𝑦}
17	7, 16, 6	wbr 5102	. . . . . . . . 9 wff 𝑎 <<s {𝑦}
18	3	cv 1568	. . . . . . . . . 10 class 𝑏
19	16, 18, 6	wbr 5102	. . . . . . . . 9 wff {𝑦} <<s 𝑏
20	17, 19	wa 401	. . . . . . . 8 wff (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)
21	20, 14, 4	crab 3412	. . . . . . 7 class {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}
22	12, 21	cima 5653	. . . . . 6 class (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
23	22	cint 4906	. . . . 5 class ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
24	13, 23	wceq 1569	. . . 4 wff (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})
25	24, 10, 21	crio 7376	. . 3 class (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)}))
26	2, 3, 5, 9, 25	cmpo 7422	. 2 class (𝑎 ∈ 𝒫 No, 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))
27	1, 26	wceq 1569	1 wff |s = (𝑎 ∈ 𝒫 No, 𝑏 ∈ ( <<s “ {𝑎}) ↦ (℩𝑥 ∈ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)} (bday‘𝑥) = ∩ (bday “ {𝑦 ∈ No ∣ (𝑎 <<s {𝑦} ∧ {𝑦} <<s 𝑏)})))

This definition is used by:  cutsval  28171  dmcuts  28182  cutsf  28183