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

Definition df-tpos 6250
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 6249 . 2  class tpos  F
3 vx . . . 4  set  x
41cdm 4705 . . . . . 6  class  dom  F
54ccnv 4704 . . . . 5  class  `' dom  F
6 c0 3468 . . . . . 6  class  (/)
76csn 3653 . . . . 5  class  { (/) }
85, 7cun 3163 . . . 4  class  ( `' dom  F  u.  { (/)
} )
93cv 1631 . . . . . . 7  class  x
109csn 3653 . . . . . 6  class  { x }
1110ccnv 4704 . . . . 5  class  `' {
x }
1211cuni 3843 . . . 4  class  U. `' { x }
133, 8, 12cmpt 4093 . . 3  class  ( x  e.  ( `' dom  F  u.  { (/) } ) 
|->  U. `' { x } )
141, 13ccom 4709 . 2  class  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )
152, 14wceq 1632 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  6251  tposssxp  6254  brtpos2  6256  tposfun  6266  dftpos2  6267  dftpos4  6269
  Copyright terms: Public domain W3C validator