Metamath Proof Explorer

Theorem lrrecval

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 No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
Assertion lrrecval Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A R B <-> A e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 lrrec.1 Could not format R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } : No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
2 eleq1 Could not format ( x = A -> ( x e. ( ( _Left ` y ) u. ( _Right ` y ) ) <-> A e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) ) : No typesetting found for |- ( x = A -> ( x e. ( ( _Left ` y ) u. ( _Right ` y ) ) <-> A e. ( ( _Left ` y ) u. ( _Right ` y ) ) ) ) with typecode |-
3 fveq2 Could not format ( y = B -> ( _Left ` y ) = ( _Left ` B ) ) : No typesetting found for |- ( y = B -> ( _Left ` y ) = ( _Left ` B ) ) with typecode |-
4 fveq2 Could not format ( y = B -> ( _Right ` y ) = ( _Right ` B ) ) : No typesetting found for |- ( y = B -> ( _Right ` y ) = ( _Right ` B ) ) with typecode |-
5 3 4 uneq12d Could not format ( y = B -> ( ( _Left ` y ) u. ( _Right ` y ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( y = B -> ( ( _Left ` y ) u. ( _Right ` y ) ) = ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
6 5 eleq2d Could not format ( y = B -> ( A e. ( ( _Left ` y ) u. ( _Right ` y ) ) <-> A e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) ) : No typesetting found for |- ( y = B -> ( A e. ( ( _Left ` y ) u. ( _Right ` y ) ) <-> A e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) ) with typecode |-
7 2 6 1 brabg Could not format ( ( A e. No /\ B e. No ) -> ( A R B <-> A e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A R B <-> A e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) ) with typecode |-