Metamath Proof Explorer


Theorem tposfo

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

Ref Expression
Assertion tposfo ( 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 → tpos 𝐹 : ( 𝐵 × 𝐴 ) –onto𝐶 )

Proof

Step Hyp Ref Expression
1 relxp Rel ( 𝐴 × 𝐵 )
2 tposfo2 ( Rel ( 𝐴 × 𝐵 ) → ( 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 → tpos 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 ) )
3 1 2 ax-mp ( 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 → tpos 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 )
4 cnvxp ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
5 foeq2 ( ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) → ( tpos 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 ↔ tpos 𝐹 : ( 𝐵 × 𝐴 ) –onto𝐶 ) )
6 4 5 ax-mp ( tpos 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 ↔ tpos 𝐹 : ( 𝐵 × 𝐴 ) –onto𝐶 )
7 3 6 sylib ( 𝐹 : ( 𝐴 × 𝐵 ) –onto𝐶 → tpos 𝐹 : ( 𝐵 × 𝐴 ) –onto𝐶 )