Metamath Proof Explorer


Theorem brprop

Description: Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses brprop.a ( 𝜑𝐴𝑉 )
brprop.b ( 𝜑𝐵𝑊 )
brprop.c ( 𝜑𝐶𝑉 )
brprop.d ( 𝜑𝐷𝑊 )
Assertion brprop ( 𝜑 → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 brprop.a ( 𝜑𝐴𝑉 )
2 brprop.b ( 𝜑𝐵𝑊 )
3 brprop.c ( 𝜑𝐶𝑉 )
4 brprop.d ( 𝜑𝐷𝑊 )
5 df-pr { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
6 5 breqi ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌𝑋 ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) 𝑌 )
7 brun ( 𝑋 ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) 𝑌 ↔ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ) )
8 6 7 bitri ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ) )
9 brsnop ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) ) )
10 1 2 9 syl2anc ( 𝜑 → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) ) )
11 brsnop ( ( 𝐶𝑉𝐷𝑊 ) → ( 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ) )
12 3 4 11 syl2anc ( 𝜑 → ( 𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ) )
13 10 12 orbi12d ( 𝜑 → ( ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ } 𝑌𝑋 { ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ) ↔ ( ( 𝑋 = 𝐴𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ) ) )
14 8 13 syl5bb ( 𝜑 → ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ) ) )