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 V A B C tpos F B A C F

Proof

Step Hyp Ref Expression
1 brtpos C V A B tpos F C B A F C
2 df-br A B tpos F C A B C tpos F
3 df-br B A F C B A C F
4 1 2 3 3bitr3g C V A B C tpos F B A C F
5 df-ot A B C = A B C
6 5 eleq1i A B C tpos F A B C tpos F
7 df-ot B A C = B A C
8 7 eleq1i B A C F B A C F
9 4 6 8 3bitr4g C V A B C tpos F B A C F