Metamath Proof Explorer

Theorem homffval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses homffval.f 
|- F = ( Homf ` C )
homffval.b 
|- B = ( Base ` C )
homffval.h 
|- H = ( Hom ` C )
Assertion homffval 
|- F = ( x e. B , y e. B |-> ( 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 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
5 4 2 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
6 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
7 6 3 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
8 7 oveqd 
 |-  ( c = C -> ( x ( Hom ` c ) y ) = ( x H y ) )
9 5 5 8 mpoeq123dv 
 |-  ( c = C -> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) = ( x e. B , y e. B |-> ( x H y ) ) )
10 df-homf 
 |-  Homf = ( c e. _V |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( x ( Hom ` c ) y ) ) )
11 2 fvexi 
 |-  B e. _V
12 11 11 mpoex 
 |-  ( x e. B , y e. B |-> ( x H y ) ) e. _V
13 9 10 12 fvmpt 
 |-  ( C e. _V -> ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) ) )
14 fvprc 
 |-  ( -. C e. _V -> ( Homf ` C ) = (/) )
15 fvprc 
 |-  ( -. C e. _V -> ( Base ` C ) = (/) )
16 2 15 eqtrid 
 |-  ( -. C e. _V -> B = (/) )
17 16 olcd 
 |-  ( -. C e. _V -> ( B = (/) \/ B = (/) ) )
18 0mpo0 
 |-  ( ( B = (/) \/ B = (/) ) -> ( x e. B , y e. B |-> ( x H y ) ) = (/) )
19 17 18 syl 
 |-  ( -. C e. _V -> ( x e. B , y e. B |-> ( x H y ) ) = (/) )
20 14 19 eqtr4d 
 |-  ( -. C e. _V -> ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) ) )
21 13 20 pm2.61i 
 |-  ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) )
22 1 21 eqtri 
 |-  F = ( x e. B , y e. B |-> ( x H y ) )