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

Metamath Proof Explorer

Theorem homfval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses homffval.f 
|- F = ( Homf ` C )
homffval.b 
|- B = ( Base ` C )
homffval.h 
|- H = ( Hom ` C )
homfval.x 
|- ( ph -> X e. B )
homfval.y 
|- ( ph -> Y e. B )
Assertion homfval 
|- ( ph -> ( X F Y ) = ( X H Y ) )

Proof

Step Hyp Ref Expression
1 homffval.f 
 |-  F = ( Homf ` C )
2 homffval.b 
 |-  B = ( Base ` C )
3 homffval.h 
 |-  H = ( Hom ` C )
4 homfval.x 
 |-  ( ph -> X e. B )
5 homfval.y 
 |-  ( ph -> Y e. B )
6 1 2 3 homffval 
 |-  F = ( x e. B , y e. B |-> ( x H y ) )
7 6 a1i 
 |-  ( ph -> F = ( x e. B , y e. B |-> ( x H y ) ) )
8 oveq12 
 |-  ( ( x = X /\ y = Y ) -> ( x H y ) = ( X H Y ) )
9 8 adantl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x H y ) = ( X H Y ) )
10 ovexd 
 |-  ( ph -> ( X H Y ) e. _V )
11 7 9 4 5 10 ovmpod 
 |-  ( ph -> ( X F Y ) = ( X H Y ) )