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 ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1oi	⊢ ( I ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐴 × 𝐵 )
2		tposf1o	⊢ ( ( I ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐴 × 𝐵 ) → tpos ( I ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 × 𝐵 ) )
3	1 2	ax-mp	⊢ tpos ( I ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 × 𝐵 )