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

Definition df-setc 15679
 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.)
Assertion
Ref Expression
df-setc comp
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-setc
StepHypRef Expression
1 csetc 15678 . 2
2 vu . . 3
3 cvv 3059 . . 3
4 cnx 14838 . . . . . 6
5 cbs 14841 . . . . . 6
64, 5cfv 5569 . . . . 5
72cv 1404 . . . . 5
86, 7cop 3978 . . . 4
9 chom 14920 . . . . . 6
104, 9cfv 5569 . . . . 5
11 vx . . . . . 6
12 vy . . . . . 6
1312cv 1404 . . . . . . 7
1411cv 1404 . . . . . . 7
15 cmap 7457 . . . . . . 7
1613, 14, 15co 6278 . . . . . 6
1711, 12, 7, 7, 16cmpt2 6280 . . . . 5
1810, 17cop 3978 . . . 4
19 cco 14921 . . . . . 6 comp
204, 19cfv 5569 . . . . 5 comp
21 vv . . . . . 6
22 vz . . . . . 6
237, 7cxp 4821 . . . . . 6
24 vg . . . . . . 7
25 vf . . . . . . 7
2622cv 1404 . . . . . . . 8
2721cv 1404 . . . . . . . . 9
28 c2nd 6783 . . . . . . . . 9
2927, 28cfv 5569 . . . . . . . 8
3026, 29, 15co 6278 . . . . . . 7
31 c1st 6782 . . . . . . . . 9
3227, 31cfv 5569 . . . . . . . 8
3329, 32, 15co 6278 . . . . . . 7
3424cv 1404 . . . . . . . 8
3525cv 1404 . . . . . . . 8
3634, 35ccom 4827 . . . . . . 7
3724, 25, 30, 33, 36cmpt2 6280 . . . . . 6
3821, 22, 23, 7, 37cmpt2 6280 . . . . 5
3920, 38cop 3978 . . . 4 comp
408, 18, 39ctp 3976 . . 3 comp
412, 3, 40cmpt 4453 . 2 comp
421, 41wceq 1405 1 comp
 Colors of variables: wff setvar class This definition is referenced by:  setcval  15680
 Copyright terms: Public domain W3C validator