# 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}=\mathrm{ExtStrCat}\left({U}\right)$
estrcbas.u ${⊢}{\phi }\to {U}\in {V}$
Assertion estrcbas ${⊢}{\phi }\to {U}={\mathrm{Base}}_{{C}}$

### Proof

Step Hyp Ref Expression
1 estrcbas.c ${⊢}{C}=\mathrm{ExtStrCat}\left({U}\right)$
2 estrcbas.u ${⊢}{\phi }\to {U}\in {V}$
3 catstr ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)⟩\right\}\mathrm{Struct}⟨1,15⟩$
4 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
5 snsstp1 ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)⟩\right\}$
6 3 4 5 strfv ${⊢}{U}\in {V}\to {U}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)⟩\right\}}$
7 2 6 syl ${⊢}{\phi }\to {U}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)⟩\right\}}$
8 eqidd ${⊢}{\phi }\to \left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)=\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)$
9 eqidd ${⊢}{\phi }\to \left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)=\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)$
10 1 2 8 9 estrcval ${⊢}{\phi }\to {C}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)⟩\right\}$
11 10 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{U}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left({x}\in {U},{y}\in {U}⟼{{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({v}\in \left({U}×{U}\right),{z}\in {U}⟼\left({g}\in \left({{\mathrm{Base}}_{{z}}}^{{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}\right),{f}\in \left({{\mathrm{Base}}_{{2}^{nd}\left({v}\right)}}^{{\mathrm{Base}}_{{1}^{st}\left({v}\right)}}\right)⟼{g}\circ {f}\right)\right)⟩\right\}}$
12 7 11 eqtr4d ${⊢}{\phi }\to {U}={\mathrm{Base}}_{{C}}$