Description: Define the right options of a surreal. This is the set of surreals that are simpler and greater than the given surreal. (Contributed by Scott Fenton, 6-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-right | |- _R = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | x |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cright | |- _R |
|
| 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 | cslt | |- |
|
| 10 | 3 | cv | |- y |
| 11 | 6 10 9 | wbr | |- x |
| 12 | 11 3 8 | crab | |- { y e. ( _Old ` ( bday ` x ) ) | x |
| 13 | 1 2 12 | cmpt | |- ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | x |
| 14 | 0 13 | wceq | |- _R = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | x |