Definition df-left 28221

Description: Define the left options of a surreal. This is the set of surreals that are simpler and less than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-left

Step	Hyp	Ref	Expression
1		cleft 28216	. 2 class L
2		vx	. . 3 setvar 𝑥
3		csur 28002	. . 3 class No
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1568	. . . . 5 class 𝑦
6	2	cv 1568	. . . . 5 class 𝑥
7		clts 28003	. . . . 5 class <s
8	5, 6, 7	wbr 5102	. . . 4 wff 𝑦 <s 𝑥
9		cbday 28004	. . . . . 6 class bday
10	6, 9	cfv 6538	. . . . 5 class (bday‘𝑥)
11		cold 28214	. . . . 5 class O
12	10, 11	cfv 6538	. . . 4 class (O‘(bday‘𝑥))
13	8, 4, 12	crab 3412	. . 3 class {𝑦 ∈ (O‘(bday‘𝑥)) ∣ 𝑦 <s 𝑥}
14	2, 3, 13	cmpt 5185	. 2 class (𝑥 ∈ No ↦ {𝑦 ∈ (O‘(bday‘𝑥)) ∣ 𝑦 <s 𝑥})
15	1, 14	wceq 1569	1 wff L = (𝑥 ∈ No ↦ {𝑦 ∈ (O‘(bday‘𝑥)) ∣ 𝑦 <s 𝑥})

This definition is used by:  leftval  28240  leftf  28246