Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-left Structured version   Visualization version   GIF version

Definition df-left 34043
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
StepHypRef Expression
1 cleft 34038 . 2 class L
2 vx . . 3 setvar 𝑥
3 csur 33852 . . 3 class No
4 vy . . . . . 6 setvar 𝑦
54cv 1538 . . . . 5 class 𝑦
62cv 1538 . . . . 5 class 𝑥
7 cslt 33853 . . . . 5 class <s
85, 6, 7wbr 5075 . . . 4 wff 𝑦 <s 𝑥
9 cbday 33854 . . . . . 6 class bday
106, 9cfv 6437 . . . . 5 class ( bday 𝑥)
11 cold 34036 . . . . 5 class O
1210, 11cfv 6437 . . . 4 class ( O ‘( bday 𝑥))
138, 4, 12crab 3069 . . 3 class {𝑦 ∈ ( O ‘( bday 𝑥)) ∣ 𝑦 <s 𝑥}
142, 3, 13cmpt 5158 . 2 class (𝑥 No ↦ {𝑦 ∈ ( O ‘( bday 𝑥)) ∣ 𝑦 <s 𝑥})
151, 14wceq 1539 1 wff L = (𝑥 No ↦ {𝑦 ∈ ( O ‘( bday 𝑥)) ∣ 𝑦 <s 𝑥})
Colors of variables: wff setvar class
This definition is referenced by:  leftval  34056  leftf  34058
  Copyright terms: Public domain W3C validator