Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-setc | Structured version Visualization version Unicode version |
Description: Definition of the category Set, relativized to a subset . Example 3.3(1) of [Adamek] p. 22. This is the category of all sets in and functions between these sets. Generally, we will take 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 |
---|---|
df-setc | comp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csetc 16725 | . 2 | |
2 | vu | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | cnx 15854 | . . . . . 6 | |
5 | cbs 15857 | . . . . . 6 | |
6 | 4, 5 | cfv 5888 | . . . . 5 |
7 | 2 | cv 1482 | . . . . 5 |
8 | 6, 7 | cop 4183 | . . . 4 |
9 | chom 15952 | . . . . . 6 | |
10 | 4, 9 | cfv 5888 | . . . . 5 |
11 | vx | . . . . . 6 | |
12 | vy | . . . . . 6 | |
13 | 12 | cv 1482 | . . . . . . 7 |
14 | 11 | cv 1482 | . . . . . . 7 |
15 | cmap 7857 | . . . . . . 7 | |
16 | 13, 14, 15 | co 6650 | . . . . . 6 |
17 | 11, 12, 7, 7, 16 | cmpt2 6652 | . . . . 5 |
18 | 10, 17 | cop 4183 | . . . 4 |
19 | cco 15953 | . . . . . 6 comp | |
20 | 4, 19 | cfv 5888 | . . . . 5 comp |
21 | vv | . . . . . 6 | |
22 | vz | . . . . . 6 | |
23 | 7, 7 | cxp 5112 | . . . . . 6 |
24 | vg | . . . . . . 7 | |
25 | vf | . . . . . . 7 | |
26 | 22 | cv 1482 | . . . . . . . 8 |
27 | 21 | cv 1482 | . . . . . . . . 9 |
28 | c2nd 7167 | . . . . . . . . 9 | |
29 | 27, 28 | cfv 5888 | . . . . . . . 8 |
30 | 26, 29, 15 | co 6650 | . . . . . . 7 |
31 | c1st 7166 | . . . . . . . . 9 | |
32 | 27, 31 | cfv 5888 | . . . . . . . 8 |
33 | 29, 32, 15 | co 6650 | . . . . . . 7 |
34 | 24 | cv 1482 | . . . . . . . 8 |
35 | 25 | cv 1482 | . . . . . . . 8 |
36 | 34, 35 | ccom 5118 | . . . . . . 7 |
37 | 24, 25, 30, 33, 36 | cmpt2 6652 | . . . . . 6 |
38 | 21, 22, 23, 7, 37 | cmpt2 6652 | . . . . 5 |
39 | 20, 38 | cop 4183 | . . . 4 comp |
40 | 8, 18, 39 | ctp 4181 | . . 3 comp |
41 | 2, 3, 40 | cmpt 4729 | . 2 comp |
42 | 1, 41 | wceq 1483 | 1 comp |
Colors of variables: wff setvar class |
This definition is referenced by: setcval 16727 |
Copyright terms: Public domain | W3C validator |