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

Proof

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