MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tpos Unicode version

Definition df-tpos 6446
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
StepHypRef Expression
1 cF . . 3  class  F
21ctpos 6445 . 2  class tpos  F
3 vx . . . 4  set  x
41cdm 4845 . . . . . 6  class  dom  F
54ccnv 4844 . . . . 5  class  `' dom  F
6 c0 3596 . . . . . 6  class  (/)
76csn 3782 . . . . 5  class  { (/) }
85, 7cun 3286 . . . 4  class  ( `' dom  F  u.  { (/)
} )
93cv 1648 . . . . . . 7  class  x
109csn 3782 . . . . . 6  class  { x }
1110ccnv 4844 . . . . 5  class  `' {
x }
1211cuni 3983 . . . 4  class  U. `' { x }
133, 8, 12cmpt 4234 . . 3  class  ( x  e.  ( `' dom  F  u.  { (/) } ) 
|->  U. `' { x } )
141, 13ccom 4849 . 2  class  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )
152, 14wceq 1649 1  wff tpos  F  =  ( F  o.  (
x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
Colors of variables: wff set class
This definition is referenced by:  tposss  6447  tposssxp  6450  brtpos2  6452  tposfun  6462  dftpos2  6463  dftpos4  6465
  Copyright terms: Public domain W3C validator