Definition df-left 33287

Description: Define the left options of a surreal. This is the set of surreals that are "closest" on the left to the given surreal. (Contributed by Scott Fenton, 17-Dec-2021.)

Assertion

Ref	Expression
df-left	⊢ L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))})

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-left

Step	Hyp	Ref	Expression
1		cleft 33282	. 2 class L
2		vx	. . 3 setvar 𝑥
3		csur 33147	. . 3 class No
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1536	. . . . . . . 8 class 𝑦
6		vz	. . . . . . . . 9 setvar 𝑧
7	6	cv 1536	. . . . . . . 8 class 𝑧
8		cslt 33148	. . . . . . . 8 class <s
9	5, 7, 8	wbr 5066	. . . . . . 7 wff 𝑦 <s 𝑧
10	2	cv 1536	. . . . . . . 8 class 𝑥
11	7, 10, 8	wbr 5066	. . . . . . 7 wff 𝑧 <s 𝑥
12	9, 11	wa 398	. . . . . 6 wff (𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥)
13		cbday 33149	. . . . . . . 8 class bday
14	5, 13	cfv 6355	. . . . . . 7 class ( bday ‘𝑦)
15	7, 13	cfv 6355	. . . . . . 7 class ( bday ‘𝑧)
16	14, 15	wcel 2114	. . . . . 6 wff ( bday ‘𝑦) ∈ ( bday ‘𝑧)
17	12, 16	wi 4	. . . . 5 wff ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))
18	17, 6, 3	wral 3138	. . . 4 wff ∀𝑧 ∈ No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))
19	10, 13	cfv 6355	. . . . 5 class ( bday ‘𝑥)
20		cold 33280	. . . . 5 class O
21	19, 20	cfv 6355	. . . 4 class ( O ‘( bday ‘𝑥))
22	18, 4, 21	crab 3142	. . 3 class {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))}
23	2, 3, 22	cmpt 5146	. 2 class (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))})
24	1, 23	wceq 1537	1 wff L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))})

This definition is referenced by: (None)