Metamath Proof Explorer


Theorem lrrecval2

Description: Next, we establish an alternate expression for R . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 R = x y | x L y R y
Assertion lrrecval2 A No B No A R B bday A bday B

Proof

Step Hyp Ref Expression
1 lrrec.1 R = x y | x L y R y
2 1 lrrecval A No B No A R B A L B R B
3 lrold L B R B = Old bday B
4 3 a1i A No B No L B R B = Old bday B
5 4 eleq2d A No B No A L B R B A Old bday B
6 bdayelon bday B On
7 oldbday bday B On A No A Old bday B bday A bday B
8 6 7 mpan A No A Old bday B bday A bday B
9 8 adantr A No B No A Old bday B bday A bday B
10 2 5 9 3bitrd A No B No A R B bday A bday B