# Metamath Proof Explorer

## Theorem funcestrcsetc

Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-2020)

Ref Expression
Hypotheses funcestrcsetc.e ${⊢}{E}=\mathrm{ExtStrCat}\left({U}\right)$
funcestrcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
funcestrcsetc.b ${⊢}{B}={\mathrm{Base}}_{{E}}$
funcestrcsetc.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
funcestrcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
funcestrcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
funcestrcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)}\right)$
Assertion funcestrcsetc ${⊢}{\phi }\to {F}\left({E}\mathrm{Func}{S}\right){G}$

### Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ${⊢}{E}=\mathrm{ExtStrCat}\left({U}\right)$
2 funcestrcsetc.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
3 funcestrcsetc.b ${⊢}{B}={\mathrm{Base}}_{{E}}$
4 funcestrcsetc.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
5 funcestrcsetc.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
6 funcestrcsetc.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
7 funcestrcsetc.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({{\mathrm{Base}}_{{y}}}^{{\mathrm{Base}}_{{x}}}\right)}\right)$
8 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
9 eqid ${⊢}\mathrm{Hom}\left({S}\right)=\mathrm{Hom}\left({S}\right)$
10 eqid ${⊢}\mathrm{Id}\left({E}\right)=\mathrm{Id}\left({E}\right)$
11 eqid ${⊢}\mathrm{Id}\left({S}\right)=\mathrm{Id}\left({S}\right)$
12 eqid ${⊢}\mathrm{comp}\left({E}\right)=\mathrm{comp}\left({E}\right)$
13 eqid ${⊢}\mathrm{comp}\left({S}\right)=\mathrm{comp}\left({S}\right)$
14 1 estrccat ${⊢}{U}\in \mathrm{WUni}\to {E}\in \mathrm{Cat}$
15 5 14 syl ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
16 2 setccat ${⊢}{U}\in \mathrm{WUni}\to {S}\in \mathrm{Cat}$
17 5 16 syl ${⊢}{\phi }\to {S}\in \mathrm{Cat}$
18 1 2 3 4 5 6 funcestrcsetclem3 ${⊢}{\phi }\to {F}:{B}⟶{C}$
19 1 2 3 4 5 6 7 funcestrcsetclem4 ${⊢}{\phi }\to {G}Fn\left({B}×{B}\right)$
20 1 2 3 4 5 6 7 funcestrcsetclem8 ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({a}{G}{b}\right):{a}\mathrm{Hom}\left({E}\right){b}⟶{F}\left({a}\right)\mathrm{Hom}\left({S}\right){F}\left({b}\right)$
21 1 2 3 4 5 6 7 funcestrcsetclem7 ${⊢}\left({\phi }\wedge {a}\in {B}\right)\to \left({a}{G}{a}\right)\left(\mathrm{Id}\left({E}\right)\left({a}\right)\right)=\mathrm{Id}\left({S}\right)\left({F}\left({a}\right)\right)$
22 1 2 3 4 5 6 7 funcestrcsetclem9 ${⊢}\left({\phi }\wedge \left({a}\in {B}\wedge {b}\in {B}\wedge {c}\in {B}\right)\wedge \left({h}\in \left({a}\mathrm{Hom}\left({E}\right){b}\right)\wedge {k}\in \left({b}\mathrm{Hom}\left({E}\right){c}\right)\right)\right)\to \left({a}{G}{c}\right)\left({k}\left(⟨{a},{b}⟩\mathrm{comp}\left({E}\right){c}\right){h}\right)=\left({b}{G}{c}\right)\left({k}\right)\left(⟨{F}\left({a}\right),{F}\left({b}\right)⟩\mathrm{comp}\left({S}\right){F}\left({c}\right)\right)\left({a}{G}{b}\right)\left({h}\right)$
23 3 4 8 9 10 11 12 13 15 17 18 19 20 21 22 isfuncd ${⊢}{\phi }\to {F}\left({E}\mathrm{Func}{S}\right){G}$