Definition df-tpos

Description: Define the transposition of a function, which is a function G = tpos F satisfying G ( x , y ) = F ( y , x ) . (Contributed by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	df-tpos	$$⊢tposF=F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	ctpos	$$classtposF$$
2		vx	$$setvarx$$
3	0	cdm	$$class\mathrm{dom}F$$
4	3	ccnv	$$class{\mathrm{dom}F}^{-1}$$
5		c0	$$class\varnothing$$
6	5	csn	$$class\left\{\varnothing \right\}$$
7	4 6	cun	$$class\left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)$$
8	2	cv	$$setvarx$$
9	8	csn	$$class\left\{x\right\}$$
10	9	ccnv	$$class{\left\{x\right\}}^{-1}$$
11	10	cuni	$$class\bigcup {\left\{x\right\}}^{-1}$$
12	2 7 11	cmpt	$$class\left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
13	0 12	ccom	$$class\left(F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)\right)$$
14	1 13	wceq	$$wfftposF=F\circ \left(x\in \left({\mathrm{dom}F}^{-1}\cup \left\{\varnothing \right\}\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$