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

Detailed syntax breakdown

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