Metamath Proof Explorer

Definition df-setc

Description: Definition of the category Set, relativized to a subset u . Example 3.3(1) of Adamek p. 22. 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)

Ref Expression
Assertion 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 ) ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csetc 
 |-  SetCat
1 vu 
 |-  u
2 cvv 
 |-  _V
3 cbs 
 |-  Base
4 cnx 
 |-  ndx
5 4 3 cfv 
 |-  ( Base ` ndx )
6 1 cv 
 |-  u
7 5 6 cop 
 |-  <. ( Base ` ndx ) , u >.
8 chom 
 |-  Hom
9 4 8 cfv 
 |-  ( Hom ` ndx )
10 vx 
 |-  x
11 vy 
 |-  y
12 11 cv 
 |-  y
13 cmap 
 |-  ^m
14 10 cv 
 |-  x
15 12 14 13 co 
 |-  ( y ^m x )
16 10 11 6 6 15 cmpo 
 |-  ( x e. u , y e. u |-> ( y ^m x ) )
17 9 16 cop 
 |-  <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >.
18 cco 
 |-  comp
19 4 18 cfv 
 |-  ( comp ` ndx )
20 vv 
 |-  v
21 6 6 cxp 
 |-  ( u X. u )
22 vz 
 |-  z
23 vg 
 |-  g
24 22 cv 
 |-  z
25 c2nd 
 |-  2nd
26 20 cv 
 |-  v
27 26 25 cfv 
 |-  ( 2nd ` v )
28 24 27 13 co 
 |-  ( z ^m ( 2nd ` v ) )
29 vf 
 |-  f
30 c1st 
 |-  1st
31 26 30 cfv 
 |-  ( 1st ` v )
32 27 31 13 co 
 |-  ( ( 2nd ` v ) ^m ( 1st ` v ) )
33 23 cv 
 |-  g
34 29 cv 
 |-  f
35 33 34 ccom 
 |-  ( g o. f )
36 23 29 28 32 35 cmpo 
 |-  ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) )
37 20 22 21 6 36 cmpo 
 |-  ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) )
38 19 37 cop 
 |-  <. ( 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 ) ) ) >.
39 7 17 38 ctp 
 |-  { <. ( 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 ) ) ) >. }
40 1 2 39 cmpt 
 |-  ( 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 ) ) ) >. } )
41 0 40 wceq 
 |-  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 ) ) ) >. } )