Description: The next step in the development of the surreals is to establish induction and recursion across left and right sets. To that end, we are going to develop a relationship R that is founded, partial, and set-like across the surreals. This first theorem just establishes the value of R . (Contributed by Scott Fenton, 19-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | lrrec.1 | |- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } |
|
| Assertion | lrrecval | |- ( ( A e. No /\ B e. No ) -> ( A R B <-> A e. ( ( _L ` B ) u. ( _R ` B ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lrrec.1 | |- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } |
|
| 2 | eleq1 | |- ( x = A -> ( x e. ( ( _L ` y ) u. ( _R ` y ) ) <-> A e. ( ( _L ` y ) u. ( _R ` y ) ) ) ) |
|
| 3 | fveq2 | |- ( y = B -> ( _L ` y ) = ( _L ` B ) ) |
|
| 4 | fveq2 | |- ( y = B -> ( _R ` y ) = ( _R ` B ) ) |
|
| 5 | 3 4 | uneq12d | |- ( y = B -> ( ( _L ` y ) u. ( _R ` y ) ) = ( ( _L ` B ) u. ( _R ` B ) ) ) |
| 6 | 5 | eleq2d | |- ( y = B -> ( A e. ( ( _L ` y ) u. ( _R ` y ) ) <-> A e. ( ( _L ` B ) u. ( _R ` B ) ) ) ) |
| 7 | 2 6 1 | brabg | |- ( ( A e. No /\ B e. No ) -> ( A R B <-> A e. ( ( _L ` B ) u. ( _R ` B ) ) ) ) |