Definition df-left

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleft	⊢ L
1		vx	⊢ 𝑥
2		csur	⊢ No
3		vy	⊢ 𝑦
4		cold	⊢ O
5		cbday	⊢ bday
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( bday ‘ 𝑥 )
8	7 4	cfv	⊢ ( O ‘ ( bday ‘ 𝑥 ) )
9	3	cv	⊢ 𝑦
10		cslt	⊢ <s
11	9 6 10	wbr	⊢ 𝑦 <s 𝑥
12	11 3 8	crab	⊢ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑦 <s 𝑥 }
13	1 2 12	cmpt	⊢ ( 𝑥 ∈ No ↦ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑦 <s 𝑥 } )
14	0 13	wceq	⊢ L = ( 𝑥 ∈ No ↦ { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑥 ) ) ∣ 𝑦 <s 𝑥 } )