Theorem tposfun

Description: The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	tposfun	$$⊢\mathrm{Fun}F\to \mathrm{Fun}tposF$$

Proof

Step	Hyp	Ref	Expression
1		funmpt	$$⊢\mathrm{Fun}\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
2		funco	$$⊢\left(\mathrm{Fun}F\wedge \mathrm{Fun}\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)\to \mathrm{Fun}\left(F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
3	1 2	mpan2	$$⊢\mathrm{Fun}F\to \mathrm{Fun}\left(F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
4		df-tpos	$$⊢tposF=F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
5	4	funeqi	$$⊢\mathrm{Fun}tposF\leftrightarrow \mathrm{Fun}\left(F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
6	3 5	sylibr	$$⊢\mathrm{Fun}F\to \mathrm{Fun}tposF$$