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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csetc | |
|
1 | vu | |
|
2 | cvv | |
|
3 | cbs | |
|
4 | cnx | |
|
5 | 4 3 | cfv | |
6 | 1 | cv | |
7 | 5 6 | cop | |
8 | chom | |
|
9 | 4 8 | cfv | |
10 | vx | |
|
11 | vy | |
|
12 | 11 | cv | |
13 | cmap | |
|
14 | 10 | cv | |
15 | 12 14 13 | co | |
16 | 10 11 6 6 15 | cmpo | |
17 | 9 16 | cop | |
18 | cco | |
|
19 | 4 18 | cfv | |
20 | vv | |
|
21 | 6 6 | cxp | |
22 | vz | |
|
23 | vg | |
|
24 | 22 | cv | |
25 | c2nd | |
|
26 | 20 | cv | |
27 | 26 25 | cfv | |
28 | 24 27 13 | co | |
29 | vf | |
|
30 | c1st | |
|
31 | 26 30 | cfv | |
32 | 27 31 13 | co | |
33 | 23 | cv | |
34 | 29 | cv | |
35 | 33 34 | ccom | |
36 | 23 29 28 32 35 | cmpo | |
37 | 20 22 21 6 36 | cmpo | |
38 | 19 37 | cop | |
39 | 7 17 38 | ctp | |
40 | 1 2 39 | cmpt | |
41 | 0 40 | wceq | |