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

Definition df-isoc 25808
Description: Function returning the isomorphisms of the category  x. The Joy of Cats p. 28. (Contributed by FL, 9-Jun-2014.)
Assertion
Ref Expression
df-isoc  |-  Iso OLD  =  ( x  e. 
Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  E. g  e.  dom  ( dom_ `  x ) ( ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) ) } )
Distinct variable group:    x, f, g

Detailed syntax breakdown of Definition df-isoc
StepHypRef Expression
1 cisoOLD 25805 . 2  class  Iso OLD
2 vx . . 3  set  x
3 ccatOLD 25752 . . 3  class  Cat OLD
4 vg . . . . . . . . 9  set  g
54cv 1622 . . . . . . . 8  class  g
62cv 1622 . . . . . . . . 9  class  x
7 cdom_ 25712 . . . . . . . . 9  class  dom_
86, 7cfv 5255 . . . . . . . 8  class  ( dom_ `  x )
95, 8cfv 5255 . . . . . . 7  class  ( (
dom_ `  x ) `  g )
10 vf . . . . . . . . 9  set  f
1110cv 1622 . . . . . . . 8  class  f
12 ccod_ 25713 . . . . . . . . 9  class  cod_
136, 12cfv 5255 . . . . . . . 8  class  ( cod_ `  x )
1411, 13cfv 5255 . . . . . . 7  class  ( (
cod_ `  x ) `  f )
159, 14wceq 1623 . . . . . 6  wff  ( (
dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )
165, 13cfv 5255 . . . . . . 7  class  ( (
cod_ `  x ) `  g )
1711, 8cfv 5255 . . . . . . 7  class  ( (
dom_ `  x ) `  f )
1816, 17wceq 1623 . . . . . 6  wff  ( (
cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )
19 co_ 25715 . . . . . . . . . 10  class  o_
206, 19cfv 5255 . . . . . . . . 9  class  ( o_
`  x )
2111, 5, 20co 5858 . . . . . . . 8  class  ( f ( o_ `  x
) g )
22 cid_ 25714 . . . . . . . . . 10  class  id_
236, 22cfv 5255 . . . . . . . . 9  class  ( id_ `  x )
249, 23cfv 5255 . . . . . . . 8  class  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  g
) )
2521, 24wceq 1623 . . . . . . 7  wff  ( f ( o_ `  x
) g )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  g ) )
265, 11, 20co 5858 . . . . . . . 8  class  ( g ( o_ `  x
) f )
2717, 23cfv 5255 . . . . . . . 8  class  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) )
2826, 27wceq 1623 . . . . . . 7  wff  ( g ( o_ `  x
) f )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  f ) )
2925, 28wa 358 . . . . . 6  wff  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x ) `  (
( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) )
3015, 18, 29w3a 934 . . . . 5  wff  ( ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) )
318cdm 4689 . . . . 5  class  dom  ( dom_ `  x )
3230, 4, 31wrex 2544 . . . 4  wff  E. g  e.  dom  ( dom_ `  x
) ( ( (
dom_ `  x ) `  g )  =  ( ( cod_ `  x
) `  f )  /\  ( ( cod_ `  x
) `  g )  =  ( ( dom_ `  x ) `  f
)  /\  ( (
f ( o_ `  x ) g )  =  ( ( id_ `  x ) `  (
( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) )
3332, 10, 31crab 2547 . . 3  class  { f  e.  dom  ( dom_ `  x )  |  E. g  e.  dom  ( dom_ `  x ) ( ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) ) }
342, 3, 33cmpt 4077 . 2  class  ( x  e.  Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  E. g  e.  dom  ( dom_ `  x )
( ( ( dom_ `  x ) `  g
)  =  ( (
cod_ `  x ) `  f )  /\  (
( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) ) } )
351, 34wceq 1623 1  wff  Iso OLD  =  ( x  e. 
Cat OLD  |->  { f  e.  dom  ( dom_ `  x )  |  E. g  e.  dom  ( dom_ `  x ) ( ( ( dom_ `  x
) `  g )  =  ( ( cod_ `  x ) `  f
)  /\  ( ( cod_ `  x ) `  g )  =  ( ( dom_ `  x
) `  f )  /\  ( ( f ( o_ `  x ) g )  =  ( ( id_ `  x
) `  ( ( dom_ `  x ) `  g ) )  /\  ( g ( o_
`  x ) f )  =  ( ( id_ `  x ) `
 ( ( dom_ `  x ) `  f
) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  isiso  25825
  Copyright terms: Public domain W3C validator