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

Metamath Proof Explorer

Theorem estrcbas

Description: Set of objects of the category of extensible structures (in a universe). (Contributed by AV, 7-Mar-2020)

Ref Expression
Hypotheses estrcbas.c ⊢ C = ExtStrCat ⁡ U
estrcbas.u ⊢ φ → U ∈ V
Assertion estrcbas ⊢ φ → U = Base C

Proof

Step Hyp Ref Expression
1 estrcbas.c ⊢ C = ExtStrCat ⁡ U
2 estrcbas.u ⊢ φ → U ∈ V
3 catstr ⊢ 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 Struct 1 15
4 baseid ⊢ Base = Slot Base ndx
5 snsstp1 ⊢ Base ndx U ⊆ 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
6 3 4 5 strfv ⊢ U ∈ V → U = Base 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
7 2 6 syl ⊢ φ → U = Base 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
8 eqidd ⊢ φ → x ∈ U , y ∈ U ⟼ Base y Base x = x ∈ U , y ∈ U ⟼ Base y Base x
9 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
10 1 2 8 9 estrcval ⊢ φ → C = 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
11 10 fveq2d ⊢ φ → Base C = Base 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
12 7 11 eqtr4d ⊢ φ → U = Base C