Metamath Proof Explorer


Theorem relbrtpos

Description: The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015)

Ref Expression
Assertion relbrtpos ( Rel 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴𝐹 𝐶 ) )

Proof

Step Hyp Ref Expression
1 reltpos Rel tpos 𝐹
2 1 a1i ( Rel 𝐹 → Rel tpos 𝐹 )
3 brrelex2 ( ( Rel tpos 𝐹 ∧ ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ) → 𝐶 ∈ V )
4 2 3 sylan ( ( Rel 𝐹 ∧ ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ) → 𝐶 ∈ V )
5 brrelex2 ( ( Rel 𝐹 ∧ ⟨ 𝐵 , 𝐴𝐹 𝐶 ) → 𝐶 ∈ V )
6 brtpos ( 𝐶 ∈ V → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴𝐹 𝐶 ) )
7 4 5 6 pm5.21nd ( Rel 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ tpos 𝐹 𝐶 ↔ ⟨ 𝐵 , 𝐴𝐹 𝐶 ) )