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

Definition df-setc 13924
Description: Definition of the category Set, relativized to a subset  u. This is the category of all sets in 
u and functions between these sets. Generally, we will take  u to be a weak universe or Grothendieck's universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-setc  |-  SetCat  =  ( u  e.  _V  |->  {
<. ( Base `  ndx ) ,  u >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( u  X.  u
) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v ) ) ,  f  e.  ( ( 2nd `  v
)  ^m  ( 1st `  v ) )  |->  ( g  o.  f ) ) ) >. } )
Distinct variable group:    f, g, u, v, x, y, z

Detailed syntax breakdown of Definition df-setc
StepHypRef Expression
1 csetc 13923 . 2  class  SetCat
2 vu . . 3  set  u
3 cvv 2801 . . 3  class  _V
4 cnx 13161 . . . . . 6  class  ndx
5 cbs 13164 . . . . . 6  class  Base
64, 5cfv 5271 . . . . 5  class  ( Base `  ndx )
72cv 1631 . . . . 5  class  u
86, 7cop 3656 . . . 4  class  <. ( Base `  ndx ) ,  u >.
9 chom 13235 . . . . . 6  class  Hom
104, 9cfv 5271 . . . . 5  class  (  Hom  `  ndx )
11 vx . . . . . 6  set  x
12 vy . . . . . 6  set  y
1312cv 1631 . . . . . . 7  class  y
1411cv 1631 . . . . . . 7  class  x
15 cmap 6788 . . . . . . 7  class  ^m
1613, 14, 15co 5874 . . . . . 6  class  ( y  ^m  x )
1711, 12, 7, 7, 16cmpt2 5876 . . . . 5  class  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x ) )
1810, 17cop 3656 . . . 4  class  <. (  Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x
) ) >.
19 cco 13236 . . . . . 6  class comp
204, 19cfv 5271 . . . . 5  class  (comp `  ndx )
21 vv . . . . . 6  set  v
22 vz . . . . . 6  set  z
237, 7cxp 4703 . . . . . 6  class  ( u  X.  u )
24 vg . . . . . . 7  set  g
25 vf . . . . . . 7  set  f
2622cv 1631 . . . . . . . 8  class  z
2721cv 1631 . . . . . . . . 9  class  v
28 c2nd 6137 . . . . . . . . 9  class  2nd
2927, 28cfv 5271 . . . . . . . 8  class  ( 2nd `  v )
3026, 29, 15co 5874 . . . . . . 7  class  ( z  ^m  ( 2nd `  v
) )
31 c1st 6136 . . . . . . . . 9  class  1st
3227, 31cfv 5271 . . . . . . . 8  class  ( 1st `  v )
3329, 32, 15co 5874 . . . . . . 7  class  ( ( 2nd `  v )  ^m  ( 1st `  v
) )
3424cv 1631 . . . . . . . 8  class  g
3525cv 1631 . . . . . . . 8  class  f
3634, 35ccom 4709 . . . . . . 7  class  ( g  o.  f )
3724, 25, 30, 33, 36cmpt2 5876 . . . . . 6  class  ( g  e.  ( z  ^m  ( 2nd `  v ) ) ,  f  e.  ( ( 2nd `  v
)  ^m  ( 1st `  v ) )  |->  ( g  o.  f ) )
3821, 22, 23, 7, 37cmpt2 5876 . . . . 5  class  ( v  e.  ( u  X.  u ) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v ) ) ,  f  e.  ( ( 2nd `  v
)  ^m  ( 1st `  v ) )  |->  ( g  o.  f ) ) )
3920, 38cop 3656 . . . 4  class  <. (comp ` 
ndx ) ,  ( v  e.  ( u  X.  u ) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v
) ) ,  f  e.  ( ( 2nd `  v )  ^m  ( 1st `  v ) ) 
|->  ( g  o.  f
) ) ) >.
408, 18, 39ctp 3655 . . 3  class  { <. (
Base `  ndx ) ,  u >. ,  <. (  Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x
) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( u  X.  u ) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v
) ) ,  f  e.  ( ( 2nd `  v )  ^m  ( 1st `  v ) ) 
|->  ( g  o.  f
) ) ) >. }
412, 3, 40cmpt 4093 . 2  class  ( u  e.  _V  |->  { <. (
Base `  ndx ) ,  u >. ,  <. (  Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x
) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( u  X.  u ) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v
) ) ,  f  e.  ( ( 2nd `  v )  ^m  ( 1st `  v ) ) 
|->  ( g  o.  f
) ) ) >. } )
421, 41wceq 1632 1  wff  SetCat  =  ( u  e.  _V  |->  {
<. ( Base `  ndx ) ,  u >. , 
<. (  Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x ) ) >. ,  <. (comp `  ndx ) ,  ( v  e.  ( u  X.  u
) ,  z  e.  u  |->  ( g  e.  ( z  ^m  ( 2nd `  v ) ) ,  f  e.  ( ( 2nd `  v
)  ^m  ( 1st `  v ) )  |->  ( g  o.  f ) ) ) >. } )
Colors of variables: wff set class
This definition is referenced by:  setcval  13925
  Copyright terms: Public domain W3C validator