Metamath Proof Explorer

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 = ( 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 ) ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cestrc 
 |-  ExtStrCat
1 vu 
 |-  u
2 cvv 
 |-  _V
3 cbs 
 |-  Base
4 cnx 
 |-  ndx
5 4 3 cfv 
 |-  ( Base ` ndx )
6 1 cv 
 |-  u
7 5 6 cop 
 |-  <. ( Base ` ndx ) , u >.
8 chom 
 |-  Hom
9 4 8 cfv 
 |-  ( Hom ` ndx )
10 vx 
 |-  x
11 vy 
 |-  y
12 11 cv 
 |-  y
13 12 3 cfv 
 |-  ( Base ` y )
14 cmap 
 |-  ^m
15 10 cv 
 |-  x
16 15 3 cfv 
 |-  ( Base ` x )
17 13 16 14 co 
 |-  ( ( Base ` y ) ^m ( Base ` x ) )
18 10 11 6 6 17 cmpo 
 |-  ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) )
19 9 18 cop 
 |-  <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >.
20 cco 
 |-  comp
21 4 20 cfv 
 |-  ( comp ` ndx )
22 vv 
 |-  v
23 6 6 cxp 
 |-  ( u X. u )
24 vz 
 |-  z
25 vg 
 |-  g
26 24 cv 
 |-  z
27 26 3 cfv 
 |-  ( Base ` z )
28 c2nd 
 |-  2nd
29 22 cv 
 |-  v
30 29 28 cfv 
 |-  ( 2nd ` v )
31 30 3 cfv 
 |-  ( Base ` ( 2nd ` v ) )
32 27 31 14 co 
 |-  ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) )
33 vf 
 |-  f
34 c1st 
 |-  1st
35 29 34 cfv 
 |-  ( 1st ` v )
36 35 3 cfv 
 |-  ( Base ` ( 1st ` v ) )
37 31 36 14 co 
 |-  ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) )
38 25 cv 
 |-  g
39 33 cv 
 |-  f
40 38 39 ccom 
 |-  ( g o. f )
41 25 33 32 37 40 cmpo 
 |-  ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) )
42 22 24 23 6 41 cmpo 
 |-  ( 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 ) ) )
43 21 42 cop 
 |-  <. ( 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 ) ) ) >.
44 7 19 43 ctp 
 |-  { <. ( 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 ) ) ) >. }
45 1 2 44 cmpt 
 |-  ( 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 ) ) ) >. } )
46 0 45 wceq 
 |-  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 ) ) ) >. } )