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	⊢ ExtStrCat = ( 𝑢 ∈ V ↦ { ⟨ ( Base ‘ ndx ) , 𝑢 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥 ∈ 𝑢 , 𝑦 ∈ 𝑢 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( 𝑢 × 𝑢 ) , 𝑧 ∈ 𝑢 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd ‘ 𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd ‘ 𝑣 ) ) ↑m ( Base ‘ ( 1st ‘ 𝑣 ) ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) ⟩ } )

Detailed syntax breakdown

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