Definition df-estrc

Description: Definition of the category ExtStr of extensible structures. This is the category whose objects are all sets in a universe u regarded as extensible structures and whose morphisms are the functions between their base sets. If a set is not a real extensible structure, it is regarded as extensible structure with an empty base set. Because of bascnvimaeqv we do not need to restrict the universe to sets which "have a base". 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. (Proposed by Mario Carneiro, 5-Mar-2020.) (Contributed by AV, 7-Mar-2020)

	Ref	Expression
Assertion	df-estrc	$$⊢\mathrm{ExtStrCat}=\left(u\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},u⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in u,y\in u⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(u\times u\right),z\in u⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cestrc	$$class\mathrm{ExtStrCat}$$
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	12 3	cfv	$$class{\mathrm{Base}}_y$$
14		cmap	$$class{\uparrow }_{𝑚}$$
15	10	cv	$$setvarx$$
16	15 3	cfv	$$class{\mathrm{Base}}_x$$
17	13 16 14	co	$$class\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$
18	10 11 6 6 17	cmpo	$$class\left(x\in u,y\in u⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)$$
19	9 18	cop	$$class⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in u,y\in u⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩$$
20		cco	$$class\mathrm{comp}$$
21	4 20	cfv	$$class\mathrm{comp}\left(\mathrm{ndx}\right)$$
22		vv	$$setvarv$$
23	6 6	cxp	$$class\left(u\times u\right)$$
24		vz	$$setvarz$$
25		vg	$$setvarg$$
26	24	cv	$$setvarz$$
27	26 3	cfv	$$class{\mathrm{Base}}_z$$
28		c2nd	$$class{2}^{nd}$$
29	22	cv	$$setvarv$$
30	29 28	cfv	$$class{2}^{nd}\left(v\right)$$
31	30 3	cfv	$$class{\mathrm{Base}}_{2^{nd}\left(v\right)}$$
32	27 31 14	co	$$class\left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right)$$
33		vf	$$setvarf$$
34		c1st	$$class{1}^{st}$$
35	29 34	cfv	$$class{1}^{st}\left(v\right)$$
36	35 3	cfv	$$class{\mathrm{Base}}_{1^{st}\left(v\right)}$$
37	31 36 14	co	$$class\left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)$$
38	25	cv	$$setvarg$$
39	33	cv	$$setvarf$$
40	38 39	ccom	$$class\left(g\circ f\right)$$
41	25 33 32 37 40	cmpo	$$class\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)$$
42	22 24 23 6 41	cmpo	$$class\left(v\in \left(u\times u\right),z\in u⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)$$
43	21 42	cop	$$class⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(u\times u\right),z\in u⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩$$
44	7 19 43	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},u⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in u,y\in u⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(u\times u\right),z\in u⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}$$
45	1 2 44	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⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(u\times u\right),z\in u⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}\right)$$
46	0 45	wceq	$$wff\mathrm{ExtStrCat}=\left(u\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},u⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(x\in u,y\in u⟼{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(v\in \left(u\times u\right),z\in u⟼\left(g\in \left({{\mathrm{Base}}_z}^{{\mathrm{Base}}_{2^{nd}\left(v\right)}}\right),f\in \left({{\mathrm{Base}}_{2^{nd}\left(v\right)}}^{{\mathrm{Base}}_{1^{st}\left(v\right)}}\right)⟼g\circ f\right)\right)⟩\right\}\right)$$