Theorem tposfo

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

	Ref	Expression
Assertion	tposfo	$$⊢F:A\times B\underset{onto}{⟶}C\to tposF:B\times A\underset{onto}{⟶}C$$

Proof

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