This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brtp

Description: A necessary and sufficient condition for two sets to be related under a binary relation which is 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	⊢ ( 𝑋 { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ , ⟨ 𝐸 , 𝐹 ⟩ } 𝑌 ↔ ( ( 𝑋 = 𝐴 ∧ 𝑌 = 𝐵 ) ∨ ( 𝑋 = 𝐶 ∧ 𝑌 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∧ 𝑌 = 𝐹 ) ) )