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	⊢ ( 𝐵 ∈ No → ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) = ( O ‘ ( bday ‘ 𝐵 ) ) )
4	3	adantl	⊢ ( ( 𝐴 ∈ 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 ‘ 𝐵 ) ) )