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