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=\left(x\in \mathrm{No}⟼\left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)|y{<}_{s}x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleft	$$classL$$
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vy	$$setvary$$
4		cold	$$class\mathrm{Old}$$
5		cbday	$$class\mathrm{bday}$$
6	1	cv	$$setvarx$$
7	6 5	cfv	$$class\mathrm{bday}\left(x\right)$$
8	7 4	cfv	$$class\mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)$$
9	3	cv	$$setvary$$
10		cslt	$$class{<}_s$$
11	9 6 10	wbr	$$wffy{<}_{s}x$$
12	11 3 8	crab	$$class\left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)|y{<}_{s}x\right\}$$
13	1 2 12	cmpt	$$class\left(x\in \mathrm{No}⟼\left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)|y{<}_{s}x\right\}\right)$$
14	0 13	wceq	$$wffL=\left(x\in \mathrm{No}⟼\left\{y\in \mathrm{Old}\left(\mathrm{bday}\left(x\right)\right)|y{<}_{s}x\right\}\right)$$