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=uVBasendxuHomndxxu,yuyxcompndxvu×u,zugz2ndv,f2ndv1stvgf

Detailed syntax breakdown

Step Hyp Ref Expression
0 csetc classSetCat
1 vu setvaru
2 cvv classV
3 cbs classBase
4 cnx classndx
5 4 3 cfv classBasendx
6 1 cv setvaru
7 5 6 cop classBasendxu
8 chom classHom
9 4 8 cfv classHomndx
10 vx setvarx
11 vy setvary
12 11 cv setvary
13 cmap class𝑚
14 10 cv setvarx
15 12 14 13 co classyx
16 10 11 6 6 15 cmpo classxu,yuyx
17 9 16 cop classHomndxxu,yuyx
18 cco classcomp
19 4 18 cfv classcompndx
20 vv setvarv
21 6 6 cxp classu×u
22 vz setvarz
23 vg setvarg
24 22 cv setvarz
25 c2nd class2nd
26 20 cv setvarv
27 26 25 cfv class2ndv
28 24 27 13 co classz2ndv
29 vf setvarf
30 c1st class1st
31 26 30 cfv class1stv
32 27 31 13 co class2ndv1stv
33 23 cv setvarg
34 29 cv setvarf
35 33 34 ccom classgf
36 23 29 28 32 35 cmpo classgz2ndv,f2ndv1stvgf
37 20 22 21 6 36 cmpo classvu×u,zugz2ndv,f2ndv1stvgf
38 19 37 cop classcompndxvu×u,zugz2ndv,f2ndv1stvgf
39 7 17 38 ctp classBasendxuHomndxxu,yuyxcompndxvu×u,zugz2ndv,f2ndv1stvgf
40 1 2 39 cmpt classuVBasendxuHomndxxu,yuyxcompndxvu×u,zugz2ndv,f2ndv1stvgf
41 0 40 wceq wffSetCat=uVBasendxuHomndxxu,yuyxcompndxvu×u,zugz2ndv,f2ndv1stvgf