Metamath Proof Explorer

Theorem tposf1o

Description: Condition of a bijective transposition. (Contributed by Zhi Wang, 5-Oct-2025)

Ref Expression
Assertion tposf1o 
|- ( F : ( A X. B ) -1-1-onto-> C -> tpos F : ( B X. A ) -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( A X. B )
2 tposf1o2 
 |-  ( Rel ( A X. B ) -> ( F : ( A X. B ) -1-1-onto-> C -> tpos F : `' ( A X. B ) -1-1-onto-> C ) )
3 1 2 ax-mp 
 |-  ( F : ( A X. B ) -1-1-onto-> C -> tpos F : `' ( A X. B ) -1-1-onto-> C )
4 cnvxp 
 |-  `' ( A X. B ) = ( B X. A )
5 f1oeq2 
 |-  ( `' ( A X. B ) = ( B X. A ) -> ( tpos F : `' ( A X. B ) -1-1-onto-> C <-> tpos F : ( B X. A ) -1-1-onto-> C ) )
6 4 5 ax-mp 
 |-  ( tpos F : `' ( A X. B ) -1-1-onto-> C <-> tpos F : ( B X. A ) -1-1-onto-> C )
7 3 6 sylib 
 |-  ( F : ( A X. B ) -1-1-onto-> C -> tpos F : ( B X. A ) -1-1-onto-> C )