Description: Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-norec | |- norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | |- F |
|
| 1 | 0 | cnorec | |- norec ( F ) |
| 2 | vx | |- x |
|
| 3 | vy | |- y |
|
| 4 | 2 | cv | |- x |
| 5 | cleft | |- _Left |
|
| 6 | 3 | cv | |- y |
| 7 | 6 5 | cfv | |- ( _Left ` y ) |
| 8 | cright | |- _Right |
|
| 9 | 6 8 | cfv | |- ( _Right ` y ) |
| 10 | 7 9 | cun | |- ( ( _Left ` y ) u. ( _Right ` y ) ) |
| 11 | 4 10 | wcel | |- x e. ( ( _Left ` y ) u. ( _Right ` y ) ) |
| 12 | 11 2 3 | copab | |- { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } |
| 13 | csur | |- No |
|
| 14 | 13 12 0 | cfrecs | |- frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) |
| 15 | 1 14 | wceq | |- norec ( F ) = frecs ( { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } , No , F ) |