Definition df-estrc 17755

Description: Definition of the category ExtStr of extensible structures. This is the category whose objects are all sets in a universe 𝑢 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 17753 we do not need to restrict the universe to sets which "have a base". Generally, we will take 𝑢 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.)

Assertion

Ref	Expression
df-estrc	⊢ ExtStrCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))⟩})

Distinct variable group:   𝑓,𝑔,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-estrc

Step	Hyp	Ref	Expression
1		cestrc 17754	. 2 class ExtStrCat
2		vu	. . 3 setvar 𝑢
3		cvv 3422	. . 3 class V
4		cnx 16822	. . . . . 6 class ndx
5		cbs 16840	. . . . . 6 class Base
6	4, 5	cfv 6418	. . . . 5 class (Base‘ndx)
7	2	cv 1538	. . . . 5 class 𝑢
8	6, 7	cop 4564	. . . 4 class ⟨(Base‘ndx), 𝑢⟩
9		chom 16899	. . . . . 6 class Hom
10	4, 9	cfv 6418	. . . . 5 class (Hom ‘ndx)
11		vx	. . . . . 6 setvar 𝑥
12		vy	. . . . . 6 setvar 𝑦
13	12	cv 1538	. . . . . . . 8 class 𝑦
14	13, 5	cfv 6418	. . . . . . 7 class (Base‘𝑦)
15	11	cv 1538	. . . . . . . 8 class 𝑥
16	15, 5	cfv 6418	. . . . . . 7 class (Base‘𝑥)
17		cmap 8573	. . . . . . 7 class ↑m
18	14, 16, 17	co 7255	. . . . . 6 class ((Base‘𝑦) ↑m (Base‘𝑥))
19	11, 12, 7, 7, 18	cmpo 7257	. . . . 5 class (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))
20	10, 19	cop 4564	. . . 4 class ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))⟩
21		cco 16900	. . . . . 6 class comp
22	4, 21	cfv 6418	. . . . 5 class (comp‘ndx)
23		vv	. . . . . 6 setvar 𝑣
24		vz	. . . . . 6 setvar 𝑧
25	7, 7	cxp 5578	. . . . . 6 class (𝑢 × 𝑢)
26		vg	. . . . . . 7 setvar 𝑔
27		vf	. . . . . . 7 setvar 𝑓
28	24	cv 1538	. . . . . . . . 9 class 𝑧
29	28, 5	cfv 6418	. . . . . . . 8 class (Base‘𝑧)
30	23	cv 1538	. . . . . . . . . 10 class 𝑣
31		c2nd 7803	. . . . . . . . . 10 class 2nd
32	30, 31	cfv 6418	. . . . . . . . 9 class (2nd ‘𝑣)
33	32, 5	cfv 6418	. . . . . . . 8 class (Base‘(2nd ‘𝑣))
34	29, 33, 17	co 7255	. . . . . . 7 class ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣)))
35		c1st 7802	. . . . . . . . . 10 class 1st
36	30, 35	cfv 6418	. . . . . . . . 9 class (1st ‘𝑣)
37	36, 5	cfv 6418	. . . . . . . 8 class (Base‘(1st ‘𝑣))
38	33, 37, 17	co 7255	. . . . . . 7 class ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣)))
39	26	cv 1538	. . . . . . . 8 class 𝑔
40	27	cv 1538	. . . . . . . 8 class 𝑓
41	39, 40	ccom 5584	. . . . . . 7 class (𝑔 ∘ 𝑓)
42	26, 27, 34, 38, 41	cmpo 7257	. . . . . 6 class (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓))
43	23, 24, 25, 7, 42	cmpo 7257	. . . . 5 class (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))
44	22, 43	cop 4564	. . . 4 class ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))⟩
45	8, 20, 44	ctp 4562	. . 3 class {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))⟩}
46	2, 3, 45	cmpt 5153	. 2 class (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))⟩})
47	1, 46	wceq 1539	1 wff ExtStrCat = (𝑢 ∈ V ↦ {⟨(Base‘ndx), 𝑢⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑢, 𝑦 ∈ 𝑢 ↦ ((Base‘𝑦) ↑m (Base‘𝑥)))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑢 × 𝑢), 𝑧 ∈ 𝑢 ↦ (𝑔 ∈ ((Base‘𝑧) ↑m (Base‘(2nd ‘𝑣))), 𝑓 ∈ ((Base‘(2nd ‘𝑣)) ↑m (Base‘(1st ‘𝑣))) ↦ (𝑔 ∘ 𝑓)))⟩})

This definition is referenced by:  estrcval  17756