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 = (u \in V ⟼ \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩, ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csetc	$class SetCat$
1		vu	$setvar u$
2		cvv	$class V$
3		cbs	$class Base$
4		cnx	$class ndx$
5	4 3	cfv	$class {Base}_{ndx}$
6	1	cv	$setvar u$
7	5 6	cop	$class ⟨{Base}_{ndx}, u⟩$
8		chom	$class Hom$
9	4 8	cfv	$class Hom (ndx)$
10		vx	$setvar x$
11		vy	$setvar y$
12	11	cv	$setvar y$
13		cmap	$class ↑_{𝑚}$
14	10	cv	$setvar x$
15	12 14 13	co	$class (y^{x})$
16	10 11 6 6 15	cmpo	$class (x \in u, y \in u ⟼ y^{x})$
17	9 16	cop	$class ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩$
18		cco	$class comp$
19	4 18	cfv	$class comp (ndx)$
20		vv	$setvar v$
21	6 6	cxp	$class (u \times u)$
22		vz	$setvar z$
23		vg	$setvar g$
24	22	cv	$setvar z$
25		c2nd	$class 2^{nd}$
26	20	cv	$setvar v$
27	26 25	cfv	$class 2^{nd} (v)$
28	24 27 13	co	$class (z^{2^{nd} (v)})$
29		vf	$setvar f$
30		c1st	$class 1^{st}$
31	26 30	cfv	$class 1^{st} (v)$
32	27 31 13	co	$class ({2^{nd} (v)}^{1^{st} (v)})$
33	23	cv	$setvar g$
34	29	cv	$setvar f$
35	33 34	ccom	$class (g \circ f)$
36	23 29 28 32 35	cmpo	$class (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f)$
37	20 22 21 6 36	cmpo	$class (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
38	19 37	cop	$class ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩$
39	7 17 38	ctp	$class \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩, ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩\}$
40	1 2 39	cmpt	$class (u \in V ⟼ \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩, ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩\})$
41	0 40	wceq	$wff SetCat = (u \in V ⟼ \{⟨{Base}_{ndx}, u⟩, ⟨Hom (ndx), (x \in u, y \in u ⟼ y^{x})⟩, ⟨comp (ndx), (v \in (u \times u), z \in u ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))⟩\})$

Metamath Proof Explorer

Definition df-setc

Detailed syntax breakdown