Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cinv Unicode version

Definition df-cinv 25827
Description: Function ( indexed by the category  x) returning the inverses of a morphism  f. (Contributed by FL, 22-Dec-2008.)
Assertion
Ref Expression
df-cinv  |-  cinv OLD  =  ( x  e. 
Cat OLD  |->  ( f  e.  dom  ( dom_ `  x )  |->  { g  e.  dom  ( dom_ `  x )  |  ( ( f ( o_
`  x ) g )  =  ( ( id_ `  x ) `
 ( ( cod_ `  x ) `  f
) )  /\  (
g ( o_ `  x ) f )  =  ( ( id_ `  x ) `  (
( dom_ `  x ) `  f ) ) ) } ) )
Distinct variable group:    x, f, g

Detailed syntax breakdown of Definition df-cinv
StepHypRef Expression
1 ccinv 25826 . 2  class  cinv OLD
2 vx . . 3  set  x
3 ccatOLD 25752 . . 3  class  Cat OLD
4 vf . . . 4  set  f
52cv 1622 . . . . . 6  class  x
6 cdom_ 25712 . . . . . 6  class  dom_
75, 6cfv 5255 . . . . 5  class  ( dom_ `  x )
87cdm 4689 . . . 4  class  dom  ( dom_ `  x )
94cv 1622 . . . . . . . 8  class  f
10 vg . . . . . . . . 9  set  g
1110cv 1622 . . . . . . . 8  class  g
12 co_ 25715 . . . . . . . . 9  class  o_
135, 12cfv 5255 . . . . . . . 8  class  ( o_
`  x )
149, 11, 13co 5858 . . . . . . 7  class  ( f ( o_ `  x
) g )
15 ccod_ 25713 . . . . . . . . . 10  class  cod_
165, 15cfv 5255 . . . . . . . . 9  class  ( cod_ `  x )
179, 16cfv 5255 . . . . . . . 8  class  ( (
cod_ `  x ) `  f )
18 cid_ 25714 . . . . . . . . 9  class  id_
195, 18cfv 5255 . . . . . . . 8  class  ( id_ `  x )
2017, 19cfv 5255 . . . . . . 7  class  ( ( id_ `  x ) `
 ( ( cod_ `  x ) `  f
) )
2114, 20wceq 1623 . . . . . 6  wff  ( f ( o_ `  x
) g )  =  ( ( id_ `  x
) `  ( ( cod_ `  x ) `  f ) )
2211, 9, 13co 5858 . . . . . . 7  class  ( g ( o_ `  x
) f )
239, 7cfv 5255 . . . . . . . 8  class  ( (
dom_ `  x ) `  f )
2423, 19cfv 5255 . . . . . . 7  class  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) )
2522, 24wceq 1623 . . . . . 6  wff  ( g ( o_ `  x
) f )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  f ) )
2621, 25wa 358 . . . . 5  wff  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x ) `  (
( cod_ `  x ) `  f ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) )
2726, 10, 8crab 2547 . . . 4  class  { g  e.  dom  ( dom_ `  x )  |  ( ( f ( o_
`  x ) g )  =  ( ( id_ `  x ) `
 ( ( cod_ `  x ) `  f
) )  /\  (
g ( o_ `  x ) f )  =  ( ( id_ `  x ) `  (
( dom_ `  x ) `  f ) ) ) }
284, 8, 27cmpt 4077 . . 3  class  ( f  e.  dom  ( dom_ `  x )  |->  { g  e.  dom  ( dom_ `  x )  |  ( ( f ( o_
`  x ) g )  =  ( ( id_ `  x ) `
 ( ( cod_ `  x ) `  f
) )  /\  (
g ( o_ `  x ) f )  =  ( ( id_ `  x ) `  (
( dom_ `  x ) `  f ) ) ) } )
292, 3, 28cmpt 4077 . 2  class  ( x  e.  Cat OLD  |->  ( f  e.  dom  ( dom_ `  x )  |->  { g  e.  dom  ( dom_ `  x )  |  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x
) `  ( ( cod_ `  x ) `  f ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) } ) )
301, 29wceq 1623 1  wff  cinv OLD  =  ( x  e. 
Cat OLD  |->  ( f  e.  dom  ( dom_ `  x )  |->  { g  e.  dom  ( dom_ `  x )  |  ( ( f ( o_
`  x ) g )  =  ( ( id_ `  x ) `
 ( ( cod_ `  x ) `  f
) )  /\  (
g ( o_ `  x ) f )  =  ( ( id_ `  x ) `  (
( dom_ `  x ) `  f ) ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  cinvlem1  25828
  Copyright terms: Public domain W3C validator