Metamath Proof Explorer


Theorem tposf

Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ 𝐶 )

Proof

Step Hyp Ref Expression
1 relxp Rel ( 𝐴 × 𝐵 )
2 tposf2 ( Rel ( 𝐴 × 𝐵 ) → ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ) )
3 1 2 ax-mp ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
4 cnvxp ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
5 4 feq2i ( tpos 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ↔ tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ 𝐶 )
6 3 5 sylib ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 → tpos 𝐹 : ( 𝐵 × 𝐴 ) ⟶ 𝐶 )