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

Definition df-tpos 5801
Description: Define the transposition of a function, which is a function  G tpos  F satisfying  G ,  F , . (Contributed by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
df-tpos tpos  F  F  o.  `' dom  F  u.  { (/) }  |->  U. `' { }
Distinct variable group:   , F

Detailed syntax breakdown of Definition df-tpos
StepHypRef Expression
1 cF . . 3  F
21ctpos 5800 . 2 tpos  F
3 vx . . . 4  setvar
41cdm 4288 . . . . . 6  dom  F
54ccnv 4287 . . . . 5  `' dom  F
6 c0 3218 . . . . . 6  (/)
76csn 3367 . . . . 5  { (/) }
85, 7cun 2909 . . . 4  `' dom  F  u.  { (/)
}
93cv 1241 . . . . . . 7
109csn 3367 . . . . . 6  { }
1110ccnv 4287 . . . . 5  `' { }
1211cuni 3571 . . . 4  U. `' { }
133, 8, 12cmpt 3809 . . 3  `' dom  F  u.  { (/) } 
|->  U. `' { }
141, 13ccom 4292 . 2  F  o.  `' dom  F  u.  { (/) }  |->  U. `' { }
152, 14wceq 1242 1 tpos  F  F  o.  `' dom  F  u.  { (/) }  |->  U. `' { }
Colors of variables: wff set class
This definition is referenced by:  tposss  5802  tposssxp  5805  brtpos2  5807  tposfun  5816  dftpos2  5817  dftpos4  5819
  Copyright terms: Public domain W3C validator