Metamath Proof Explorer

Theorem funcf2

Description: The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcixp.b 
|- B = ( Base ` D )
funcixp.h 
|- H = ( Hom ` D )
funcixp.j 
|- J = ( Hom ` E )
funcixp.f 
|- ( ph -> F ( D Func E ) G )
funcf2.x 
|- ( ph -> X e. B )
funcf2.y 
|- ( ph -> Y e. B )
Assertion funcf2 
|- ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 funcixp.b 
 |-  B = ( Base ` D )
2 funcixp.h 
 |-  H = ( Hom ` D )
3 funcixp.j 
 |-  J = ( Hom ` E )
4 funcixp.f 
 |-  ( ph -> F ( D Func E ) G )
5 funcf2.x 
 |-  ( ph -> X e. B )
6 funcf2.y 
 |-  ( ph -> Y e. B )
7 df-ov 
 |-  ( X G Y ) = ( G ` <. X , Y >. )
8 1 2 3 4 funcixp 
 |-  ( ph -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
9 5 6 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
10 2fveq3 
 |-  ( z = <. X , Y >. -> ( F ` ( 1st ` z ) ) = ( F ` ( 1st ` <. X , Y >. ) ) )
11 2fveq3 
 |-  ( z = <. X , Y >. -> ( F ` ( 2nd ` z ) ) = ( F ` ( 2nd ` <. X , Y >. ) ) )
12 10 11 oveq12d 
 |-  ( z = <. X , Y >. -> ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) = ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) )
13 fveq2 
 |-  ( z = <. X , Y >. -> ( H ` z ) = ( H ` <. X , Y >. ) )
14 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
15 13 14 eqtr4di 
 |-  ( z = <. X , Y >. -> ( H ` z ) = ( X H Y ) )
16 12 15 oveq12d 
 |-  ( z = <. X , Y >. -> ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) ^m ( X H Y ) ) )
17 16 fvixp 
 |-  ( ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ <. X , Y >. e. ( B X. B ) ) -> ( G ` <. X , Y >. ) e. ( ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) ^m ( X H Y ) ) )
18 8 9 17 syl2anc 
 |-  ( ph -> ( G ` <. X , Y >. ) e. ( ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) ^m ( X H Y ) ) )
19 7 18 eqeltrid 
 |-  ( ph -> ( X G Y ) e. ( ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) ^m ( X H Y ) ) )
20 op1stg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
21 20 fveq2d 
 |-  ( ( X e. B /\ Y e. B ) -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
22 op2ndg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
23 22 fveq2d 
 |-  ( ( X e. B /\ Y e. B ) -> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) )
24 21 23 oveq12d 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) = ( ( F ` X ) J ( F ` Y ) ) )
25 5 6 24 syl2anc 
 |-  ( ph -> ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) = ( ( F ` X ) J ( F ` Y ) ) )
26 25 oveq1d 
 |-  ( ph -> ( ( ( F ` ( 1st ` <. X , Y >. ) ) J ( F ` ( 2nd ` <. X , Y >. ) ) ) ^m ( X H Y ) ) = ( ( ( F ` X ) J ( F ` Y ) ) ^m ( X H Y ) ) )
27 19 26 eleqtrd 
 |-  ( ph -> ( X G Y ) e. ( ( ( F ` X ) J ( F ` Y ) ) ^m ( X H Y ) ) )
28 elmapi 
 |-  ( ( X G Y ) e. ( ( ( F ` X ) J ( F ` Y ) ) ^m ( X H Y ) ) -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
29 27 28 syl 
 |-  ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )