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 ⊢ B ∈ No → L ⁡ B ∪ R ⁡ B = Old ⁡ bday ⁡ B
4 3 adantl ⊢ 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