This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V ⟼ Base ndx u Hom ⁡ ndx x ∈ u , y ∈ u ⟼ Base y Base x comp ⁡ ndx v ∈ u × u , z ∈ u ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cestrc class ExtStrCat
1 vu setvar u
2 cvv class V
3 cbs class Base
4 cnx class ndx
5 4 3 cfv class Base ndx
6 1 cv setvar u
7 5 6 cop class Base ndx u
8 chom class Hom
9 4 8 cfv class Hom ⁡ ndx
10 vx setvar x
11 vy setvar y
12 11 cv setvar y
13 12 3 cfv class Base y
14 cmap class ↑ 𝑚
15 10 cv setvar x
16 15 3 cfv class Base x
17 13 16 14 co class Base y Base x
18 10 11 6 6 17 cmpo class x ∈ u , y ∈ u ⟼ Base y Base x
19 9 18 cop class Hom ⁡ ndx x ∈ u , y ∈ u ⟼ Base y Base x
20 cco class comp
21 4 20 cfv class comp ⁡ ndx
22 vv setvar v
23 6 6 cxp class u × u
24 vz setvar z
25 vg setvar g
26 24 cv setvar z
27 26 3 cfv class Base z
28 c2nd class 2 nd
29 22 cv setvar v
30 29 28 cfv class 2 nd ⁡ v
31 30 3 cfv class Base 2 nd ⁡ v
32 27 31 14 co class Base z Base 2 nd ⁡ v
33 vf setvar f
34 c1st class 1 st
35 29 34 cfv class 1 st ⁡ v
36 35 3 cfv class Base 1 st ⁡ v
37 31 36 14 co class Base 2 nd ⁡ v Base 1 st ⁡ v
38 25 cv setvar g
39 33 cv setvar f
40 38 39 ccom class g ∘ f
41 25 33 32 37 40 cmpo class g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f
42 22 24 23 6 41 cmpo class v ∈ u × u , z ∈ u ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f
43 21 42 cop class comp ⁡ ndx v ∈ u × u , z ∈ u ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f
44 7 19 43 ctp class Base ndx u Hom ⁡ ndx x ∈ u , y ∈ u ⟼ Base y Base x comp ⁡ ndx v ∈ u × u , z ∈ u ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f
45 1 2 44 cmpt class u ∈ V ⟼ Base ndx u Hom ⁡ ndx x ∈ u , y ∈ u ⟼ Base y Base x comp ⁡ ndx v ∈ u × u , z ∈ u ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f
46 0 45 wceq wff ExtStrCat = u ∈ V ⟼ Base ndx u Hom ⁡ ndx x ∈ u , y ∈ u ⟼ Base y Base x comp ⁡ ndx v ∈ u × u , z ∈ u ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f