Theorem tposf1o

Description: Condition of a bijective transposition. (Contributed by Zhi Wang, 5-Oct-2025)

	Ref	Expression
Assertion	tposf1o	$$⊢F:A\times B\underset{1-1\; onto}{⟶}C\to tposF:B\times A\underset{1-1\; onto}{⟶}C$$

Proof

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