Definition df-left 31933

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 = ( x e. No |-> { y e. ( O ` ( bday ` x ) ) | A. z e. No ( ( y <s z /\ z <s x ) -> ( bday ` y ) e. ( bday ` z ) ) } )

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-left

Step	Hyp	Ref	Expression
1		cleft 31928	. 2 class L
2		vx	. . 3 setvar x
3		csur 31793	. . 3 class No
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1482	. . . . . . . 8 class y
6		vz	. . . . . . . . 9 setvar z
7	6	cv 1482	. . . . . . . 8 class z
8		cslt 31794	. . . . . . . 8 class <s
9	5, 7, 8	wbr 4653	. . . . . . 7 wff y <s z
10	2	cv 1482	. . . . . . . 8 class x
11	7, 10, 8	wbr 4653	. . . . . . 7 wff z <s x
12	9, 11	wa 384	. . . . . 6 wff ( y <s z /\ z <s x )
13		cbday 31795	. . . . . . . 8 class bday
14	5, 13	cfv 5888	. . . . . . 7 class ( bday ` y )
15	7, 13	cfv 5888	. . . . . . 7 class ( bday ` z )
16	14, 15	wcel 1990	. . . . . 6 wff ( bday ` y ) e. ( bday ` z )
17	12, 16	wi 4	. . . . 5 wff ( ( y <s z /\ z <s x ) -> ( bday ` y ) e. ( bday ` z ) )
18	17, 6, 3	wral 2912	. . . 4 wff A. z e. No ( ( y <s z /\ z <s x ) -> ( bday ` y ) e. ( bday ` z ) )
19	10, 13	cfv 5888	. . . . 5 class ( bday ` x )
20		cold 31926	. . . . 5 class O
21	19, 20	cfv 5888	. . . 4 class ( O ` ( bday ` x ) )
22	18, 4, 21	crab 2916	. . 3 class { y e. ( O ` ( bday ` x ) ) | A. z e. No ( ( y <s z /\ z <s x ) -> ( bday ` y ) e. ( bday ` z ) ) }
23	2, 3, 22	cmpt 4729	. 2 class ( x e. No |-> { y e. ( O ` ( bday ` x ) ) | A. z e. No ( ( y <s z /\ z <s x ) -> ( bday ` y ) e. ( bday ` z ) ) } )
24	1, 23	wceq 1483	1 wff L = ( x e. No |-> { y e. ( O ` ( bday ` x ) ) | A. z e. No ( ( y <s z /\ z <s x ) -> ( bday ` y ) e. ( bday ` z ) ) } )

This definition is referenced by: (None)