Theorem tposresxp

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

	Ref	Expression
Assertion	tposresxp	$$⊢{tposF\upharpoonright }_{\left(A\times B\right)}=tpos\left({F\upharpoonright }_{\left(B\times A\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(A\times B\right)$$
2		tposres	$$⊢\mathrm{Rel}\left(A\times B\right)\to {tposF\upharpoonright }_{\left(A\times B\right)}=tpos\left({F\upharpoonright }_{{\left(A\times B\right)}^{-1}}\right)$$
3	1 2	ax-mp	$$⊢{tposF\upharpoonright }_{\left(A\times B\right)}=tpos\left({F\upharpoonright }_{{\left(A\times B\right)}^{-1}}\right)$$
4		cnvxp	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$
5	4	reseq2i	$$⊢{F\upharpoonright }_{{\left(A\times B\right)}^{-1}}={F\upharpoonright }_{\left(B\times A\right)}$$
6	5	tposeqi	$$⊢tpos\left({F\upharpoonright }_{{\left(A\times B\right)}^{-1}}\right)=tpos\left({F\upharpoonright }_{\left(B\times A\right)}\right)$$
7	3 6	eqtri	$$⊢{tposF\upharpoonright }_{\left(A\times B\right)}=tpos\left({F\upharpoonright }_{\left(B\times A\right)}\right)$$