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

Definition df-setc 14223
 Description: Definition of the category Set, relativized to a subset . This is the category of all sets in and functions between these sets. Generally, we will take to be a weak universe or Grothendieck's 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 comp
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-setc
StepHypRef Expression
1 csetc 14222 . 2
2 vu . . 3
3 cvv 2948 . . 3
4 cnx 13458 . . . . . 6
5 cbs 13461 . . . . . 6
64, 5cfv 5446 . . . . 5
72cv 1651 . . . . 5
86, 7cop 3809 . . . 4
9 chom 13532 . . . . . 6
104, 9cfv 5446 . . . . 5
11 vx . . . . . 6
12 vy . . . . . 6
1312cv 1651 . . . . . . 7
1411cv 1651 . . . . . . 7
15 cmap 7010 . . . . . . 7
1613, 14, 15co 6073 . . . . . 6
1711, 12, 7, 7, 16cmpt2 6075 . . . . 5
1810, 17cop 3809 . . . 4
19 cco 13533 . . . . . 6 comp
204, 19cfv 5446 . . . . 5 comp
21 vv . . . . . 6
22 vz . . . . . 6
237, 7cxp 4868 . . . . . 6
24 vg . . . . . . 7
25 vf . . . . . . 7
2622cv 1651 . . . . . . . 8
2721cv 1651 . . . . . . . . 9
28 c2nd 6340 . . . . . . . . 9
2927, 28cfv 5446 . . . . . . . 8
3026, 29, 15co 6073 . . . . . . 7
31 c1st 6339 . . . . . . . . 9
3227, 31cfv 5446 . . . . . . . 8
3329, 32, 15co 6073 . . . . . . 7
3424cv 1651 . . . . . . . 8
3525cv 1651 . . . . . . . 8
3634, 35ccom 4874 . . . . . . 7
3724, 25, 30, 33, 36cmpt2 6075 . . . . . 6
3821, 22, 23, 7, 37cmpt2 6075 . . . . 5
3920, 38cop 3809 . . . 4 comp
408, 18, 39ctp 3808 . . 3 comp
412, 3, 40cmpt 4258 . 2 comp
421, 41wceq 1652 1 comp
 Colors of variables: wff set class This definition is referenced by:  setcval  14224
 Copyright terms: Public domain W3C validator