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

Metamath Proof Explorer

Theorem ottpos

Description: The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Assertion ottpos 
|- ( C e. V -> ( <. A , B , C >. e. tpos F <-> <. B , A , C >. e. F ) )

Proof

Step Hyp Ref Expression
1 brtpos 
 |-  ( C e. V -> ( <. A , B >. tpos F C <-> <. B , A >. F C ) )
2 df-br 
 |-  ( <. A , B >. tpos F C <-> <. <. A , B >. , C >. e. tpos F )
3 df-br 
 |-  ( <. B , A >. F C <-> <. <. B , A >. , C >. e. F )
4 1 2 3 3bitr3g 
 |-  ( C e. V -> ( <. <. A , B >. , C >. e. tpos F <-> <. <. B , A >. , C >. e. F ) )
5 df-ot 
 |-  <. A , B , C >. = <. <. A , B >. , C >.
6 5 eleq1i 
 |-  ( <. A , B , C >. e. tpos F <-> <. <. A , B >. , C >. e. tpos F )
7 df-ot 
 |-  <. B , A , C >. = <. <. B , A >. , C >.
8 7 eleq1i 
 |-  ( <. B , A , C >. e. F <-> <. <. B , A >. , C >. e. F )
9 4 6 8 3bitr4g 
 |-  ( C e. V -> ( <. A , B , C >. e. tpos F <-> <. B , A , C >. e. F ) )