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

Definition df-tpos 6923
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 6922 . 2  class tpos  F
3 vx . . . 4  setvar  x
41cdm 4791 . . . . . 6  class  dom  F
54ccnv 4790 . . . . 5  class  `' dom  F
6 c0 3699 . . . . . 6  class  (/)
76csn 3936 . . . . 5  class  { (/) }
85, 7cun 3372 . . . 4  class  ( `' dom  F  u.  { (/)
} )
93cv 1436 . . . . . . 7  class  x
109csn 3936 . . . . . 6  class  { x }
1110ccnv 4790 . . . . 5  class  `' {
x }
1211cuni 4157 . . . 4  class  U. `' { x }
133, 8, 12cmpt 4420 . . 3  class  ( x  e.  ( `' dom  F  u.  { (/) } ) 
|->  U. `' { x } )
141, 13ccom 4795 . 2  class  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )
152, 14wceq 1437 1  wff tpos  F  =  ( F  o.  (
x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
Colors of variables: wff setvar class
This definition is referenced by:  tposss  6924  tposssxp  6927  brtpos2  6929  tposfun  6939  dftpos2  6940  dftpos4  6942
  Copyright terms: Public domain W3C validator