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

Metamath Proof Explorer

Theorem estrccofval

Description: Composition in the category of extensible structures. (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c ⊢ C = ExtStrCat ⁡ U
estrcbas.u ⊢ φ → U ∈ V
estrcco.o ⊢ · ˙ = comp ⁡ C
Assertion estrccofval ⊢ φ → · ˙ = v ∈ U × U , z ∈ U ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f

Proof

Step Hyp Ref Expression
1 estrcbas.c ⊢ C = ExtStrCat ⁡ U
2 estrcbas.u ⊢ φ → U ∈ V
3 estrcco.o ⊢ · ˙ = comp ⁡ C
4 eqid ⊢ Hom ⁡ C = Hom ⁡ C
5 1 2 4 estrchomfval ⊢ φ → Hom ⁡ C = x ∈ U , y ∈ U ⟼ Base y Base x
6 eqidd ⊢ φ → v ∈ U × U , z ∈ U ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f = v ∈ U × U , z ∈ U ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f
7 1 2 5 6 estrcval ⊢ φ → C = Base ndx U Hom ⁡ ndx Hom ⁡ C 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
8 catstr ⊢ Base ndx U Hom ⁡ ndx Hom ⁡ C 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 Struct 1 15
9 ccoid ⊢ comp = Slot comp ⁡ ndx
10 snsstp3 ⊢ 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 ⊆ Base ndx U Hom ⁡ ndx Hom ⁡ C 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
11 2 2 xpexd ⊢ φ → U × U ∈ V
12 mpoexga ⊢ U × U ∈ V ∧ U ∈ V → v ∈ U × U , z ∈ U ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f ∈ V
13 11 2 12 syl2anc ⊢ φ → v ∈ U × U , z ∈ U ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f ∈ V
14 7 8 9 10 13 3 strfv3 ⊢ φ → · ˙ = v ∈ U × U , z ∈ U ⟼ g ∈ Base z Base 2 nd ⁡ v , f ∈ Base 2 nd ⁡ v Base 1 st ⁡ v ⟼ g ∘ f