Theorem tposco

Description: Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	tposco	$$⊢tpos\left(F\circ G\right)=F\circ tposG$$

Proof

Step	Hyp	Ref	Expression
1		coass	$$⊢\left(F\circ G\right)\circ \left(x\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)=F\circ \left(G\circ \left(x\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
2		dftpos4	$$⊢tpos\left(F\circ G\right)=\left(F\circ G\right)\circ \left(x\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
3		dftpos4	$$⊢tposG=G\circ \left(x\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
4	3	coeq2i	$$⊢F\circ tposG=F\circ \left(G\circ \left(x\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
5	1 2 4	3eqtr4i	$$⊢tpos\left(F\circ G\right)=F\circ tposG$$