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

Definition df-setc 15032
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 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 15031 . 2  class  SetCat
2 vu . . 3  setvar  u
3 cvv 3054 . . 3  class  _V
4 cnx 14259 . . . . . 6  class  ndx
5 cbs 14262 . . . . . 6  class  Base
64, 5cfv 5502 . . . . 5  class  ( Base `  ndx )
72cv 1369 . . . . 5  class  u
86, 7cop 3967 . . . 4  class  <. ( Base `  ndx ) ,  u >.
9 chom 14337 . . . . . 6  class  Hom
104, 9cfv 5502 . . . . 5  class  ( Hom  `  ndx )
11 vx . . . . . 6  setvar  x
12 vy . . . . . 6  setvar  y
1312cv 1369 . . . . . . 7  class  y
1411cv 1369 . . . . . . 7  class  x
15 cmap 7300 . . . . . . 7  class  ^m
1613, 14, 15co 6176 . . . . . 6  class  ( y  ^m  x )
1711, 12, 7, 7, 16cmpt2 6178 . . . . 5  class  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x ) )
1810, 17cop 3967 . . . 4  class  <. ( Hom  `  ndx ) ,  ( x  e.  u ,  y  e.  u  |->  ( y  ^m  x
) ) >.
19 cco 14338 . . . . . 6  class comp
204, 19cfv 5502 . . . . 5  class  (comp `  ndx )
21 vv . . . . . 6  setvar  v
22 vz . . . . . 6  setvar  z
237, 7cxp 4922 . . . . . 6  class  ( u  X.  u )
24 vg . . . . . . 7  setvar  g
25 vf . . . . . . 7  setvar  f
2622cv 1369 . . . . . . . 8  class  z
2721cv 1369 . . . . . . . . 9  class  v
28 c2nd 6662 . . . . . . . . 9  class  2nd
2927, 28cfv 5502 . . . . . . . 8  class  ( 2nd `  v )
3026, 29, 15co 6176 . . . . . . 7  class  ( z  ^m  ( 2nd `  v
) )
31 c1st 6661 . . . . . . . . 9  class  1st
3227, 31cfv 5502 . . . . . . . 8  class  ( 1st `  v )
3329, 32, 15co 6176 . . . . . . 7  class  ( ( 2nd `  v )  ^m  ( 1st `  v
) )
3424cv 1369 . . . . . . . 8  class  g
3525cv 1369 . . . . . . . 8  class  f
3634, 35ccom 4928 . . . . . . 7  class  ( g  o.  f )
3724, 25, 30, 33, 36cmpt2 6178 . . . . . 6  class  ( g  e.  ( z  ^m  ( 2nd `  v ) ) ,  f  e.  ( ( 2nd `  v
)  ^m  ( 1st `  v ) )  |->  ( g  o.  f ) )
3821, 22, 23, 7, 37cmpt2 6178 . . . . 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 3967 . . . 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 3965 . . 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 4434 . 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 1370 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 setvar class
This definition is referenced by:  setcval  15033
  Copyright terms: Public domain W3C validator