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	|- X e. _V
	brtp.2	|- Y e. _V
Assertion	brtp	|- ( X { <. A , B >. , <. C , D >. , <. E , F >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) \/ ( X = E /\ Y = F ) ) )

Proof

Step	Hyp	Ref	Expression
1		brtp.1	|- X e. _V
2		brtp.2	|- Y e. _V
3		df-br	|- ( X { <. A , B >. , <. C , D >. , <. E , F >. } Y <-> <. X , Y >. e. { <. A , B >. , <. C , D >. , <. E , F >. } )
4		opex	|- <. X , Y >. e. _V
5	4	eltp	|- ( <. X , Y >. e. { <. A , B >. , <. C , D >. , <. E , F >. } <-> ( <. X , Y >. = <. A , B >. \/ <. X , Y >. = <. C , D >. \/ <. X , Y >. = <. E , F >. ) )
6	1 2	opth	|- ( <. X , Y >. = <. A , B >. <-> ( X = A /\ Y = B ) )
7	1 2	opth	|- ( <. X , Y >. = <. C , D >. <-> ( X = C /\ Y = D ) )
8	1 2	opth	|- ( <. X , Y >. = <. E , F >. <-> ( X = E /\ Y = F ) )
9	6 7 8	3orbi123i	|- ( ( <. X , Y >. = <. A , B >. \/ <. X , Y >. = <. C , D >. \/ <. X , Y >. = <. E , F >. ) <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) \/ ( X = E /\ Y = F ) ) )
10	3 5 9	3bitri	|- ( X { <. A , B >. , <. C , D >. , <. E , F >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) \/ ( X = E /\ Y = F ) ) )