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

Definition df-iso 13652
Description: Function returning the isomorphisms of the category  c. The Joy of Cats p. 28. (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 13649 . 2  class  Iso
2 vc . . 3  set  c
3 ccat 13566 . . 3  class  Cat
4 vx . . . . 5  set  x
5 cvv 2788 . . . . 5  class  _V
64cv 1622 . . . . . 6  class  x
76cdm 4689 . . . . 5  class  dom  x
84, 5, 7cmpt 4077 . . . 4  class  ( x  e.  _V  |->  dom  x
)
92cv 1622 . . . . 5  class  c
10 cinv 13648 . . . . 5  class Inv
119, 10cfv 5255 . . . 4  class  (Inv `  c )
128, 11ccom 4693 . . 3  class  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) )
132, 3, 12cmpt 4077 . 2  class  ( c  e.  Cat  |->  ( ( x  e.  _V  |->  dom  x )  o.  (Inv `  c ) ) )
141, 13wceq 1623 1  wff  Iso  =  ( c  e.  Cat  |->  ( ( x  e. 
_V  |->  dom  x )  o.  (Inv `  c )
) )
Colors of variables: wff set class
This definition is referenced by:  isoval  13667
  Copyright terms: Public domain W3C validator