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\in V\to \left(⟨A,B,C⟩\in tposF\leftrightarrow ⟨B,A,C⟩\in F\right)$$

Proof

Step	Hyp	Ref	Expression
1		brtpos	$$⊢C\in V\to \left(⟨A,B⟩tposFC\leftrightarrow ⟨B,A⟩FC\right)$$
2		df-br	$$⊢⟨A,B⟩tposFC\leftrightarrow ⟨⟨A,B⟩,C⟩\in tposF$$
3		df-br	$$⊢⟨B,A⟩FC\leftrightarrow ⟨⟨B,A⟩,C⟩\in F$$
4	1 2 3	3bitr3g	$$⊢C\in V\to \left(⟨⟨A,B⟩,C⟩\in tposF\leftrightarrow ⟨⟨B,A⟩,C⟩\in F\right)$$
5		df-ot	$$⊢⟨A,B,C⟩=⟨⟨A,B⟩,C⟩$$
6	5	eleq1i	$$⊢⟨A,B,C⟩\in tposF\leftrightarrow ⟨⟨A,B⟩,C⟩\in tposF$$
7		df-ot	$$⊢⟨B,A,C⟩=⟨⟨B,A⟩,C⟩$$
8	7	eleq1i	$$⊢⟨B,A,C⟩\in F\leftrightarrow ⟨⟨B,A⟩,C⟩\in F$$
9	4 6 8	3bitr4g	$$⊢C\in V\to \left(⟨A,B,C⟩\in tposF\leftrightarrow ⟨B,A,C⟩\in F\right)$$