This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( C evalF D )
evlf1.c 
|- ( ph -> C e. Cat )
evlf1.d 
|- ( ph -> D e. Cat )
evlf1.b 
|- B = ( Base ` C )
evlf1.f 
|- ( ph -> F e. ( C Func D ) )
evlf1.x 
|- ( ph -> X e. B )
Assertion evlf1 
|- ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )

Proof

Step Hyp Ref Expression
1 evlf1.e 
 |-  E = ( C evalF D )
2 evlf1.c 
 |-  ( ph -> C e. Cat )
3 evlf1.d 
 |-  ( ph -> D e. Cat )
4 evlf1.b 
 |-  B = ( Base ` C )
5 evlf1.f 
 |-  ( ph -> F e. ( C Func D ) )
6 evlf1.x 
 |-  ( ph -> X e. B )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 eqid 
 |-  ( comp ` D ) = ( comp ` D )
9 eqid 
 |-  ( C Nat D ) = ( C Nat D )
10 1 2 3 4 7 8 9 evlfval 
 |-  ( ph -> E = <. ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( C Nat D ) n ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. )
11 ovex 
 |-  ( C Func D ) e. _V
12 4 fvexi 
 |-  B e. _V
13 11 12 mpoex 
 |-  ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) e. _V
14 11 12 xpex 
 |-  ( ( C Func D ) X. B ) e. _V
15 14 14 mpoex 
 |-  ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( C Nat D ) n ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) e. _V
16 13 15 op1std 
 |-  ( E = <. ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) , ( x e. ( ( C Func D ) X. B ) , y e. ( ( C Func D ) X. B ) |-> [_ ( 1st ` x ) / m ]_ [_ ( 1st ` y ) / n ]_ ( a e. ( m ( C Nat D ) n ) , g e. ( ( 2nd ` x ) ( Hom ` C ) ( 2nd ` y ) ) |-> ( ( a ` ( 2nd ` y ) ) ( <. ( ( 1st ` m ) ` ( 2nd ` x ) ) , ( ( 1st ` m ) ` ( 2nd ` y ) ) >. ( comp ` D ) ( ( 1st ` n ) ` ( 2nd ` y ) ) ) ( ( ( 2nd ` x ) ( 2nd ` m ) ( 2nd ` y ) ) ` g ) ) ) ) >. -> ( 1st ` E ) = ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) )
17 10 16 syl 
 |-  ( ph -> ( 1st ` E ) = ( f e. ( C Func D ) , x e. B |-> ( ( 1st ` f ) ` x ) ) )
18 simprl 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> f = F )
19 18 fveq2d 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> ( 1st ` f ) = ( 1st ` F ) )
20 simprr 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> x = X )
21 19 20 fveq12d 
 |-  ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( 1st ` f ) ` x ) = ( ( 1st ` F ) ` X ) )
22 fvexd 
 |-  ( ph -> ( ( 1st ` F ) ` X ) e. _V )
23 17 21 5 6 22 ovmpod 
 |-  ( ph -> ( F ( 1st ` E ) X ) = ( ( 1st ` F ) ` X ) )