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