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	|- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) }
Assertion	lrrecval	|- ( ( A e. No /\ B e. No ) -> ( A R B <-> A e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) )

Proof

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