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 R = x y | x L y R y
Assertion lrrecval A No B No A R B A L B R B

Proof

Step Hyp Ref Expression
1 lrrec.1 R = x y | x L y R y
2 eleq1 x = A x L y R y A L y 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 R y = L B R B
6 5 eleq2d y = B A L y R y A L B R B
7 2 6 1 brabg A No B No A R B A L B R B