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=\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}$$
Assertion	lrrecval	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(ARB\leftrightarrow A\in \left(L\left(B\right)\cup R\left(B\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lrrec.1	$$⊢R=\left\{⟨x,y⟩|x\in \left(L\left(y\right)\cup R\left(y\right)\right)\right\}$$
2		eleq1	$$⊢x=A\to \left(x\in \left(L\left(y\right)\cup R\left(y\right)\right)\leftrightarrow A\in \left(L\left(y\right)\cup R\left(y\right)\right)\right)$$
3		fveq2	$$⊢y=B\to L\left(y\right)=L\left(B\right)$$
4		fveq2	$$⊢y=B\to R\left(y\right)=R\left(B\right)$$
5	3 4	uneq12d	$$⊢y=B\to L\left(y\right)\cup R\left(y\right)=L\left(B\right)\cup R\left(B\right)$$
6	5	eleq2d	$$⊢y=B\to \left(A\in \left(L\left(y\right)\cup R\left(y\right)\right)\leftrightarrow A\in \left(L\left(B\right)\cup R\left(B\right)\right)\right)$$
7	2 6 1	brabg	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(ARB\leftrightarrow A\in \left(L\left(B\right)\cup R\left(B\right)\right)\right)$$