Metamath Proof Explorer


Theorem brtp

Description: A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011)

Ref Expression
Hypotheses brtp.1 𝑋 ∈ V
brtp.2 𝑌 ∈ V
Assertion brtp ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ∨ ( 𝑋 = 𝐸𝑌 = 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 brtp.1 𝑋 ∈ V
2 brtp.2 𝑌 ∈ V
3 df-br ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } )
4 opex 𝑋 , 𝑌 ⟩ ∈ V
5 4 eltp ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } ↔ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∨ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ ) )
6 1 2 opth ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑋 = 𝐴𝑌 = 𝐵 ) )
7 1 2 opth ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑋 = 𝐶𝑌 = 𝐷 ) )
8 1 2 opth ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( 𝑋 = 𝐸𝑌 = 𝐹 ) )
9 6 7 8 3orbi123i ( ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∨ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ ) ↔ ( ( 𝑋 = 𝐴𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ∨ ( 𝑋 = 𝐸𝑌 = 𝐹 ) ) )
10 3 5 9 3bitri ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶𝑌 = 𝐷 ) ∨ ( 𝑋 = 𝐸𝑌 = 𝐹 ) ) )