ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tpos Unicode version

Definition df-tpos 6271
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 6270 . 2  class tpos  F
3 vx . . . 4  setvar  x
41cdm 4644 . . . . . 6  class  dom  F
54ccnv 4643 . . . . 5  class  `' dom  F
6 c0 3437 . . . . . 6  class  (/)
76csn 3607 . . . . 5  class  { (/) }
85, 7cun 3142 . . . 4  class  ( `' dom  F  u.  { (/)
} )
93cv 1363 . . . . . . 7  class  x
109csn 3607 . . . . . 6  class  { x }
1110ccnv 4643 . . . . 5  class  `' {
x }
1211cuni 3824 . . . 4  class  U. `' { x }
133, 8, 12cmpt 4079 . . 3  class  ( x  e.  ( `' dom  F  u.  { (/) } ) 
|->  U. `' { x } )
141, 13ccom 4648 . 2  class  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )
152, 14wceq 1364 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  6272  tposssxp  6275  brtpos2  6277  tposfun  6286  dftpos2  6287  dftpos4  6289
  Copyright terms: Public domain W3C validator