Definition df-tpos 6999

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.)

Assertion

Ref	Expression
df-tpos	|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )

Distinct variable group:   x, F

Detailed syntax breakdown of Definition df-tpos

Step	Hyp	Ref	Expression
1		cF	. . 3 class F
2	1	ctpos 6998	. 2 class tpos F
3		vx	. . . 4 setvar x
4	1	cdm 4853	. . . . . 6 class dom F
5	4	ccnv 4852	. . . . 5 class `' dom F
6		c0 3743	. . . . . 6 class (/)
7	6	csn 3980	. . . . 5 class { (/) }
8	5, 7	cun 3414	. . . 4 class ( `' dom F u. { (/) } )
9	3	cv 1454	. . . . . . 7 class x
10	9	csn 3980	. . . . . 6 class { x }
11	10	ccnv 4852	. . . . 5 class `' { x }
12	11	cuni 4212	. . . 4 class U. `' { x }
13	3, 8, 12	cmpt 4475	. . 3 class ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } )
14	1, 13	ccom 4857	. 2 class ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
15	2, 14	wceq 1455	1 wff tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )

This definition is referenced by:  tposss  7000  tposssxp  7003  brtpos2  7005  tposfun  7015  dftpos2  7016  dftpos4  7018