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	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ tpos 𝐹 ↔ ⟨ 𝐵 , 𝐴 , 𝐶 ⟩ ∈ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		brtpos	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ) )
2		df-br	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ tpos 𝐹 )
3		df-br	⊢ ( ⟨ 𝐵 , 𝐴 ⟩ 𝐹 𝐶 ↔ ⟨ ⟨ 𝐵 , 𝐴 ⟩ , 𝐶 ⟩ ∈ 𝐹 )
4	1 2 3	3bitr3g	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ tpos 𝐹 ↔ ⟨ ⟨ 𝐵 , 𝐴 ⟩ , 𝐶 ⟩ ∈ 𝐹 ) )
5		df-ot	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
6	5	eleq1i	⊢ ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ tpos 𝐹 ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ tpos 𝐹 )
7		df-ot	⊢ ⟨ 𝐵 , 𝐴 , 𝐶 ⟩ = ⟨ ⟨ 𝐵 , 𝐴 ⟩ , 𝐶 ⟩
8	7	eleq1i	⊢ ( ⟨ 𝐵 , 𝐴 , 𝐶 ⟩ ∈ 𝐹 ↔ ⟨ ⟨ 𝐵 , 𝐴 ⟩ , 𝐶 ⟩ ∈ 𝐹 )
9	4 6 8	3bitr4g	⊢ ( 𝐶 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ tpos 𝐹 ↔ ⟨ 𝐵 , 𝐴 , 𝐶 ⟩ ∈ 𝐹 ) )