Theorem tposf1o2

Description: Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015)

	Ref	Expression
Assertion	tposf1o2	$$⊢\mathrm{Rel}A\to \left(F:A\underset{1-1\; onto}{⟶}B\to tposF:A^{-1}\underset{1-1\; onto}{⟶}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposf12	$$⊢\mathrm{Rel}A\to \left(F:A\underset{1-1}{⟶}B\to tposF:A^{-1}\underset{1-1}{⟶}B\right)$$
2		tposfo2	$$⊢\mathrm{Rel}A\to \left(F:A\underset{onto}{⟶}B\to tposF:A^{-1}\underset{onto}{⟶}B\right)$$
3	1 2	anim12d	$$⊢\mathrm{Rel}A\to \left(\left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)\to \left(tposF:A^{-1}\underset{1-1}{⟶}B\wedge tposF:A^{-1}\underset{onto}{⟶}B\right)\right)$$
4		df-f1o	$$⊢F:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{1-1}{⟶}B\wedge F:A\underset{onto}{⟶}B\right)$$
5		df-f1o	$$⊢tposF:A^{-1}\underset{1-1\; onto}{⟶}B\leftrightarrow \left(tposF:A^{-1}\underset{1-1}{⟶}B\wedge tposF:A^{-1}\underset{onto}{⟶}B\right)$$
6	3 4 5	3imtr4g	$$⊢\mathrm{Rel}A\to \left(F:A\underset{1-1\; onto}{⟶}B\to tposF:A^{-1}\underset{1-1\; onto}{⟶}B\right)$$