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 No typesetting found for |- R = { <. x , y >. | x e. ( ( _Left ` y ) u. ( _Right ` y ) ) } with typecode |-
Assertion lrrecval2 ANoBNoARBbdayAbdayB

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 1 lrrecval 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 |-
3 lrold Could not format ( ( _Left ` B ) u. ( _Right ` B ) ) = ( _Old ` ( bday ` B ) ) : No typesetting found for |- ( ( _Left ` B ) u. ( _Right ` B ) ) = ( _Old ` ( bday ` B ) ) with typecode |-
4 3 a1i Could not format ( ( A e. No /\ B e. No ) -> ( ( _Left ` B ) u. ( _Right ` B ) ) = ( _Old ` ( bday ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( _Left ` B ) u. ( _Right ` B ) ) = ( _Old ` ( bday ` B ) ) ) with typecode |-
5 4 eleq2d Could not format ( ( A e. No /\ B e. No ) -> ( A e. ( ( _Left ` B ) u. ( _Right ` B ) ) <-> A e. ( _Old ` ( bday ` B ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A e. ( ( _Left ` B ) u. ( _Right ` B ) ) <-> A e. ( _Old ` ( bday ` B ) ) ) ) with typecode |-
6 bdayelon bdayBOn
7 oldbday bdayBOnANoAOldbdayBbdayAbdayB
8 6 7 mpan ANoAOldbdayBbdayAbdayB
9 8 adantr ANoBNoAOldbdayBbdayAbdayB
10 2 5 9 3bitrd ANoBNoARBbdayAbdayB