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

Definition df-tpos 5891
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 5890 . 2  class tpos  F
3 vx . . . 4  setvar  x
41cdm 4373 . . . . . 6  class  dom  F
54ccnv 4372 . . . . 5  class  `' dom  F
6 c0 3252 . . . . . 6  class  (/)
76csn 3403 . . . . 5  class  { (/) }
85, 7cun 2943 . . . 4  class  ( `' dom  F  u.  { (/)
} )
93cv 1258 . . . . . . 7  class  x
109csn 3403 . . . . . 6  class  { x }
1110ccnv 4372 . . . . 5  class  `' {
x }
1211cuni 3608 . . . 4  class  U. `' { x }
133, 8, 12cmpt 3846 . . 3  class  ( x  e.  ( `' dom  F  u.  { (/) } ) 
|->  U. `' { x } )
141, 13ccom 4377 . 2  class  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/) } )  |->  U. `' { x } ) )
152, 14wceq 1259 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  5892  tposssxp  5895  brtpos2  5897  tposfun  5906  dftpos2  5907  dftpos4  5909
  Copyright terms: Public domain W3C validator