Definition df-estrc 16763

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 16761 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.)

Assertion

Ref	Expression
df-estrc	|- ExtStrCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } )

Distinct variable group:   f, g, u, v, x, y, z

Detailed syntax breakdown of Definition df-estrc

Step	Hyp	Ref	Expression
1		cestrc 16762	. 2 class ExtStrCat
2		vu	. . 3 setvar u
3		cvv 3200	. . 3 class _V
4		cnx 15854	. . . . . 6 class ndx
5		cbs 15857	. . . . . 6 class Base
6	4, 5	cfv 5888	. . . . 5 class ( Base ` ndx )
7	2	cv 1482	. . . . 5 class u
8	6, 7	cop 4183	. . . 4 class <. ( Base ` ndx ) , u >.
9		chom 15952	. . . . . 6 class Hom
10	4, 9	cfv 5888	. . . . 5 class ( Hom ` ndx )
11		vx	. . . . . 6 setvar x
12		vy	. . . . . 6 setvar y
13	12	cv 1482	. . . . . . . 8 class y
14	13, 5	cfv 5888	. . . . . . 7 class ( Base ` y )
15	11	cv 1482	. . . . . . . 8 class x
16	15, 5	cfv 5888	. . . . . . 7 class ( Base ` x )
17		cmap 7857	. . . . . . 7 class ^m
18	14, 16, 17	co 6650	. . . . . 6 class ( ( Base ` y ) ^m ( Base ` x ) )
19	11, 12, 7, 7, 18	cmpt2 6652	. . . . 5 class ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) )
20	10, 19	cop 4183	. . . 4 class <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >.
21		cco 15953	. . . . . 6 class comp
22	4, 21	cfv 5888	. . . . 5 class (comp ` ndx )
23		vv	. . . . . 6 setvar v
24		vz	. . . . . 6 setvar z
25	7, 7	cxp 5112	. . . . . 6 class ( u X. u )
26		vg	. . . . . . 7 setvar g
27		vf	. . . . . . 7 setvar f
28	24	cv 1482	. . . . . . . . 9 class z
29	28, 5	cfv 5888	. . . . . . . 8 class ( Base ` z )
30	23	cv 1482	. . . . . . . . . 10 class v
31		c2nd 7167	. . . . . . . . . 10 class 2nd
32	30, 31	cfv 5888	. . . . . . . . 9 class ( 2nd ` v )
33	32, 5	cfv 5888	. . . . . . . 8 class ( Base ` ( 2nd ` v ) )
34	29, 33, 17	co 6650	. . . . . . 7 class ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) )
35		c1st 7166	. . . . . . . . . 10 class 1st
36	30, 35	cfv 5888	. . . . . . . . 9 class ( 1st ` v )
37	36, 5	cfv 5888	. . . . . . . 8 class ( Base ` ( 1st ` v ) )
38	33, 37, 17	co 6650	. . . . . . 7 class ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) )
39	26	cv 1482	. . . . . . . 8 class g
40	27	cv 1482	. . . . . . . 8 class f
41	39, 40	ccom 5118	. . . . . . 7 class ( g o. f )
42	26, 27, 34, 38, 41	cmpt2 6652	. . . . . 6 class ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) )
43	23, 24, 25, 7, 42	cmpt2 6652	. . . . 5 class ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) )
44	22, 43	cop 4183	. . . 4 class <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >.
45	8, 20, 44	ctp 4181	. . 3 class { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. }
46	2, 3, 45	cmpt 4729	. 2 class ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } )
47	1, 46	wceq 1483	1 wff ExtStrCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) >. } )

This definition is referenced by:  estrcval  16764