Metamath Proof Explorer


Theorem funcsetcestrc

Description: The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 28-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s S=SetCatU
funcsetcestrc.c C=BaseS
funcsetcestrc.f φF=xCBasendxx
funcsetcestrc.u φUWUni
funcsetcestrc.o φωU
funcsetcestrc.g φG=xC,yCIyx
funcsetcestrc.e E=ExtStrCatU
Assertion funcsetcestrc φFSFuncEG

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s S=SetCatU
2 funcsetcestrc.c C=BaseS
3 funcsetcestrc.f φF=xCBasendxx
4 funcsetcestrc.u φUWUni
5 funcsetcestrc.o φωU
6 funcsetcestrc.g φG=xC,yCIyx
7 funcsetcestrc.e E=ExtStrCatU
8 eqid BaseE=BaseE
9 eqid HomS=HomS
10 eqid HomE=HomE
11 eqid IdS=IdS
12 eqid IdE=IdE
13 eqid compS=compS
14 eqid compE=compE
15 1 setccat UWUniSCat
16 4 15 syl φSCat
17 7 estrccat UWUniECat
18 4 17 syl φECat
19 1 2 3 4 5 7 8 funcsetcestrclem3 φF:CBaseE
20 1 2 3 4 5 6 funcsetcestrclem4 φGFnC×C
21 1 2 3 4 5 6 7 funcsetcestrclem8 φaCbCaGb:aHomSbFaHomEFb
22 1 2 3 4 5 6 7 funcsetcestrclem7 φaCaGaIdSa=IdEFa
23 1 2 3 4 5 6 7 funcsetcestrclem9 φaCbCcChaHomSbkbHomScaGckabcompSch=bGckFaFbcompEFcaGbh
24 2 8 9 10 11 12 13 14 16 18 19 20 21 22 23 isfuncd φFSFuncEG