Metamath Proof Explorer

Theorem tposidf1o

Description: The swap function, or the twisting map, is bijective. (Contributed by Zhi Wang, 5-Oct-2025)

Ref Expression
Assertion tposidf1o 
|- tpos ( _I |` ( A X. B ) ) : ( B X. A ) -1-1-onto-> ( A X. B )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` ( A X. B ) ) : ( A X. B ) -1-1-onto-> ( A X. B )
2 tposf1o 
 |-  ( ( _I |` ( A X. B ) ) : ( A X. B ) -1-1-onto-> ( A X. B ) -> tpos ( _I |` ( A X. B ) ) : ( B X. A ) -1-1-onto-> ( A X. B ) )
3 1 2 ax-mp 
 |-  tpos ( _I |` ( A X. B ) ) : ( B X. A ) -1-1-onto-> ( A X. B )