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 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 ) ) )