Metamath Proof Explorer


Theorem setccofval

Description: Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcbas.c C=SetCatU
setcbas.u φUV
setcco.o ·˙=compC
Assertion setccofval φ·˙=vU×U,zUgz2ndv,f2ndv1stvgf

Proof

Step Hyp Ref Expression
1 setcbas.c C=SetCatU
2 setcbas.u φUV
3 setcco.o ·˙=compC
4 eqid HomC=HomC
5 1 2 4 setchomfval φHomC=xU,yUyx
6 eqidd φvU×U,zUgz2ndv,f2ndv1stvgf=vU×U,zUgz2ndv,f2ndv1stvgf
7 1 2 5 6 setcval φC=BasendxUHomndxHomCcompndxvU×U,zUgz2ndv,f2ndv1stvgf
8 catstr BasendxUHomndxHomCcompndxvU×U,zUgz2ndv,f2ndv1stvgfStruct115
9 ccoid comp=Slotcompndx
10 snsstp3 compndxvU×U,zUgz2ndv,f2ndv1stvgfBasendxUHomndxHomCcompndxvU×U,zUgz2ndv,f2ndv1stvgf
11 2 2 xpexd φU×UV
12 mpoexga U×UVUVvU×U,zUgz2ndv,f2ndv1stvgfV
13 11 2 12 syl2anc φvU×U,zUgz2ndv,f2ndv1stvgfV
14 7 8 9 10 13 3 strfv3 φ·˙=vU×U,zUgz2ndv,f2ndv1stvgf