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

Definition df-idcatset 26043
Description: The identity morphims in the category Set. Experimental. (Contributed by FL, 6-Nov-2013.)
Assertion
Ref Expression
df-idcatset  |-  Id SetCat  =  ( x  e.  Univ  |->  ( a  e.  x  |-> 
<. <. a ,  a
>. ,  (  _I  |`  a ) >. )
)
Distinct variable group:    x, a

Detailed syntax breakdown of Definition df-idcatset
StepHypRef Expression
1 cidcase 26042 . 2  class  Id SetCat
2 vx . . 3  set  x
3 cgru 8428 . . 3  class  Univ
4 va . . . 4  set  a
52cv 1631 . . . 4  class  x
64cv 1631 . . . . . 6  class  a
76, 6cop 3656 . . . . 5  class  <. a ,  a >.
8 cid 4320 . . . . . 6  class  _I
98, 6cres 4707 . . . . 5  class  (  _I  |`  a )
107, 9cop 3656 . . . 4  class  <. <. a ,  a >. ,  (  _I  |`  a ) >.
114, 5, 10cmpt 4093 . . 3  class  ( a  e.  x  |->  <. <. a ,  a >. ,  (  _I  |`  a ) >. )
122, 3, 11cmpt 4093 . 2  class  ( x  e.  Univ  |->  ( a  e.  x  |->  <. <. a ,  a >. ,  (  _I  |`  a ) >. ) )
131, 12wceq 1632 1  wff  Id SetCat  =  ( x  e.  Univ  |->  ( a  e.  x  |-> 
<. <. a ,  a
>. ,  (  _I  |`  a ) >. )
)
Colors of variables: wff set class
This definition is referenced by:  idcatfun  26044  idmor  26049
  Copyright terms: Public domain W3C validator