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

Definition df-catset 25389
Description: Definition of the category Set. (We should say "the categories Set" since there is such a category per universe but for our purpose they are equivalent obviously.) Experimental. (Contributed by FL, 8-Nov-2013.)
Assertion
Ref Expression
df-catset  |-  SetCat OLD  =  ( x  e.  Univ  |->  <. <. ( dom SetCat `  x
) ,  ( cod SetCat `
 x ) >. ,  <. ( Id SetCat `  x ) ,  ( ro SetCat `  x ) >. >. )

Detailed syntax breakdown of Definition df-catset
StepHypRef Expression
1 ccaset 25388 . 2  class  SetCat OLD
2 vx . . 3  set  x
3 cgru 8412 . . 3  class  Univ
42cv 1622 . . . . . 6  class  x
5 cdomcase 25331 . . . . . 6  class  dom SetCat
64, 5cfv 5255 . . . . 5  class  ( dom SetCat `
 x )
7 ccodcase 25344 . . . . . 6  class  cod SetCat
84, 7cfv 5255 . . . . 5  class  ( cod SetCat `
 x )
96, 8cop 3643 . . . 4  class  <. ( dom
SetCat `  x ) ,  ( cod SetCat `  x
) >.
10 cidcase 25351 . . . . . 6  class  Id SetCat
114, 10cfv 5255 . . . . 5  class  ( Id SetCat `
 x )
12 crocase 25367 . . . . . 6  class  ro SetCat
134, 12cfv 5255 . . . . 5  class  ( ro SetCat `
 x )
1411, 13cop 3643 . . . 4  class  <. ( Id SetCat `  x ) ,  ( ro SetCat `  x ) >.
159, 14cop 3643 . . 3  class  <. <. ( dom
SetCat `  x ) ,  ( cod SetCat `  x
) >. ,  <. ( Id SetCat `  x ) ,  ( ro SetCat `  x ) >. >.
162, 3, 15cmpt 4077 . 2  class  ( x  e.  Univ  |->  <. <. ( dom
SetCat `  x ) ,  ( cod SetCat `  x
) >. ,  <. ( Id SetCat `  x ) ,  ( ro SetCat `  x ) >. >. )
171, 16wceq 1623 1  wff  SetCat OLD  =  ( x  e.  Univ  |->  <. <. ( dom SetCat `  x
) ,  ( cod SetCat `
 x ) >. ,  <. ( Id SetCat `  x ) ,  ( ro SetCat `  x ) >. >. )
Colors of variables: wff set class
This definition is referenced by:  iscatset  25390
  Copyright terms: Public domain W3C validator