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 = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | y |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cleft | |- _L |
|
| 1 | vx | |- x |
|
| 2 | csur | |- No |
|
| 3 | vy | |- y |
|
| 4 | cold | |- _Old |
|
| 5 | cbday | |- bday |
|
| 6 | 1 | cv | |- x |
| 7 | 6 5 | cfv | |- ( bday ` x ) |
| 8 | 7 4 | cfv | |- ( _Old ` ( bday ` x ) ) |
| 9 | 3 | cv | |- y |
| 10 | cslt | |- |
|
| 11 | 9 6 10 | wbr | |- y |
| 12 | 11 3 8 | crab | |- { y e. ( _Old ` ( bday ` x ) ) | y |
| 13 | 1 2 12 | cmpt | |- ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | y |
| 14 | 0 13 | wceq | |- _L = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | y |