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	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1	0	ctpos	|- tpos F
2		vx	|- x
3	0	cdm	|- dom F
4	3	ccnv	|- `' dom F
5		c0	|- (/)
6	5	csn	|- { (/) }
7	4 6	cun	|- ( `' dom F u. { (/) } )
8	2	cv	|- x
9	8	csn	|- { x }
10	9	ccnv	|- `' { x }
11	10	cuni	|- U. `' { x }
12	2 7 11	cmpt	|- ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
13	0 12	ccom	|- ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
14	1 13	wceq	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )