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 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion lrrecval2 ( ( 𝐴 No 𝐵 No ) → ( 𝐴 𝑅 𝐵 ↔ ( bday 𝐴 ) ∈ ( bday 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lrrec.1 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
2 1 lrrecval ( ( 𝐴 No 𝐵 No ) → ( 𝐴 𝑅 𝐵𝐴 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ) )
3 lrold ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) = ( O ‘ ( bday 𝐵 ) )
4 3 a1i ( ( 𝐴 No 𝐵 No ) → ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) = ( O ‘ ( bday 𝐵 ) ) )
5 4 eleq2d ( ( 𝐴 No 𝐵 No ) → ( 𝐴 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ↔ 𝐴 ∈ ( O ‘ ( bday 𝐵 ) ) ) )
6 bdayelon ( bday 𝐵 ) ∈ On
7 oldbday ( ( ( bday 𝐵 ) ∈ On ∧ 𝐴 No ) → ( 𝐴 ∈ ( O ‘ ( bday 𝐵 ) ) ↔ ( bday 𝐴 ) ∈ ( bday 𝐵 ) ) )
8 6 7 mpan ( 𝐴 No → ( 𝐴 ∈ ( O ‘ ( bday 𝐵 ) ) ↔ ( bday 𝐴 ) ∈ ( bday 𝐵 ) ) )
9 8 adantr ( ( 𝐴 No 𝐵 No ) → ( 𝐴 ∈ ( O ‘ ( bday 𝐵 ) ) ↔ ( bday 𝐴 ) ∈ ( bday 𝐵 ) ) )
10 2 5 9 3bitrd ( ( 𝐴 No 𝐵 No ) → ( 𝐴 𝑅 𝐵 ↔ ( bday 𝐴 ) ∈ ( bday 𝐵 ) ) )