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	$⊢ X \in V$
		brtp.2	$⊢ Y \in V$
	Assertion	brtp	$⊢ X \{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\} Y \leftrightarrow ((X = A \land Y = B) \lor (X = C \land Y = D) \lor (X = E \land Y = F))$

Proof

Step	Hyp	Ref	Expression
1		brtp.1	$⊢ X \in V$
2		brtp.2	$⊢ Y \in V$
3		df-br	$⊢ X \{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\} Y \leftrightarrow ⟨X, Y⟩ \in \{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\}$
4		opex	$⊢ ⟨X, Y⟩ \in V$
5	4	eltp	$⊢ ⟨X, Y⟩ \in \{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\} \leftrightarrow (⟨X, Y⟩ = ⟨A, B⟩ \lor ⟨X, Y⟩ = ⟨C, D⟩ \lor ⟨X, Y⟩ = ⟨E, F⟩)$
6	1 2	opth	$⊢ ⟨X, Y⟩ = ⟨A, B⟩ \leftrightarrow (X = A \land Y = B)$
7	1 2	opth	$⊢ ⟨X, Y⟩ = ⟨C, D⟩ \leftrightarrow (X = C \land Y = D)$
8	1 2	opth	$⊢ ⟨X, Y⟩ = ⟨E, F⟩ \leftrightarrow (X = E \land Y = F)$
9	6 7 8	3orbi123i	$⊢ (⟨X, Y⟩ = ⟨A, B⟩ \lor ⟨X, Y⟩ = ⟨C, D⟩ \lor ⟨X, Y⟩ = ⟨E, F⟩) \leftrightarrow ((X = A \land Y = B) \lor (X = C \land Y = D) \lor (X = E \land Y = F))$
10	3 5 9	3bitri	$⊢ X \{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\} Y \leftrightarrow ((X = A \land Y = B) \lor (X = C \land Y = D) \lor (X = E \land Y = F))$