Theorem tposresxp

Description: The transposition restricted to a Cartesian product. (Contributed by Zhi Wang, 6-Oct-2025)

	Ref	Expression
Assertion	tposresxp	⊢ ( tpos 𝐹 ↾ ( 𝐴 × 𝐵 ) ) = tpos ( 𝐹 ↾ ( 𝐵 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relxp	⊢ Rel ( 𝐴 × 𝐵 )
2		tposres	⊢ ( Rel ( 𝐴 × 𝐵 ) → ( tpos 𝐹 ↾ ( 𝐴 × 𝐵 ) ) = tpos ( 𝐹 ↾ ◡ ( 𝐴 × 𝐵 ) ) )
3	1 2	ax-mp	⊢ ( tpos 𝐹 ↾ ( 𝐴 × 𝐵 ) ) = tpos ( 𝐹 ↾ ◡ ( 𝐴 × 𝐵 ) )
4		cnvxp	⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
5	4	reseq2i	⊢ ( 𝐹 ↾ ◡ ( 𝐴 × 𝐵 ) ) = ( 𝐹 ↾ ( 𝐵 × 𝐴 ) )
6	5	tposeqi	⊢ tpos ( 𝐹 ↾ ◡ ( 𝐴 × 𝐵 ) ) = tpos ( 𝐹 ↾ ( 𝐵 × 𝐴 ) )
7	3 6	eqtri	⊢ ( tpos 𝐹 ↾ ( 𝐴 × 𝐵 ) ) = tpos ( 𝐹 ↾ ( 𝐵 × 𝐴 ) )