Metamath Proof Explorer


Theorem evlf1

Description: Value of the evaluation functor at an object. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses evlf1.e E=CevalFD
evlf1.c φCCat
evlf1.d φDCat
evlf1.b B=BaseC
evlf1.f φFCFuncD
evlf1.x φXB
Assertion evlf1 φF1stEX=1stFX

Proof

Step Hyp Ref Expression
1 evlf1.e E=CevalFD
2 evlf1.c φCCat
3 evlf1.d φDCat
4 evlf1.b B=BaseC
5 evlf1.f φFCFuncD
6 evlf1.x φXB
7 eqid HomC=HomC
8 eqid compD=compD
9 eqid CNatD=CNatD
10 1 2 3 4 7 8 9 evlfval φE=fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namCNatDn,g2ndxHomC2ndya2ndy1stm2ndx1stm2ndycompD1stn2ndy2ndx2ndm2ndyg
11 ovex CFuncDV
12 4 fvexi BV
13 11 12 mpoex fCFuncD,xB1stfxV
14 11 12 xpex CFuncD×BV
15 14 14 mpoex xCFuncD×B,yCFuncD×B1stx/m1sty/namCNatDn,g2ndxHomC2ndya2ndy1stm2ndx1stm2ndycompD1stn2ndy2ndx2ndm2ndygV
16 13 15 op1std E=fCFuncD,xB1stfxxCFuncD×B,yCFuncD×B1stx/m1sty/namCNatDn,g2ndxHomC2ndya2ndy1stm2ndx1stm2ndycompD1stn2ndy2ndx2ndm2ndyg1stE=fCFuncD,xB1stfx
17 10 16 syl φ1stE=fCFuncD,xB1stfx
18 simprl φf=Fx=Xf=F
19 18 fveq2d φf=Fx=X1stf=1stF
20 simprr φf=Fx=Xx=X
21 19 20 fveq12d φf=Fx=X1stfx=1stFX
22 fvexd φ1stFXV
23 17 21 5 6 22 ovmpod φF1stEX=1stFX