Theorem tposf

Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)

	Ref	Expression
Assertion	tposf	$$⊢F:A\times B⟶C\to tposF:B\times A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(A\times B\right)$$
2		tposf2	$$⊢\mathrm{Rel}\left(A\times B\right)\to \left(F:A\times B⟶C\to tposF:{\left(A\times B\right)}^{-1}⟶C\right)$$
3	1 2	ax-mp	$$⊢F:A\times B⟶C\to tposF:{\left(A\times B\right)}^{-1}⟶C$$
4		cnvxp	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$
5	4	feq2i	$$⊢tposF:{\left(A\times B\right)}^{-1}⟶C\leftrightarrow tposF:B\times A⟶C$$
6	3 5	sylib	$$⊢F:A\times B⟶C\to tposF:B\times A⟶C$$