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

Definition df-iso 15360
Description: Function returning the isomorphisms of the category  c. Definition 3.8 of [Adamek] p. 28, and definition in [Lang] p. 54. (Contributed by FL, 9-Jun-2014.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-iso  |-  Iso  =  ( c  e.  Cat  |->  ( ( x  e. 
_V  |->  dom  x )  o.  (Inv `  c )
) )
Distinct variable group:    x, c

Detailed syntax breakdown of Definition df-iso
StepHypRef Expression
1 ciso 15357 . 2  class  Iso
2 vc . . 3  setvar  c
3 ccat 15276 . . 3  class  Cat
4 vx . . . . 5  setvar  x
5 cvv 3058 . . . . 5  class  _V
64cv 1404 . . . . . 6  class  x
76cdm 4822 . . . . 5  class  dom  x
84, 5, 7cmpt 4452 . . . 4  class  ( x  e.  _V  |->  dom  x
)
92cv 1404 . . . . 5  class  c
10 cinv 15356 . . . . 5  class Inv
119, 10cfv 5568 . . . 4  class  (Inv `  c )
128, 11ccom 4826 . . 3  class  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) )
132, 3, 12cmpt 4452 . 2  class  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
141, 13wceq 1405 1  wff  Iso  =  ( c  e.  Cat  |->  ( ( x  e. 
_V  |->  dom  x )  o.  (Inv `  c )
) )
Colors of variables: wff setvar class
This definition is referenced by:  isofval  15368
  Copyright terms: Public domain W3C validator