Metamath Proof Explorer

Theorem funcixp

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 )
Assertion funcixp 
|- ( ph -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )

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 eqid 
 |-  ( Base ` E ) = ( Base ` E )
6 eqid 
 |-  ( Id ` D ) = ( Id ` D )
7 eqid 
 |-  ( Id ` E ) = ( Id ` E )
8 eqid 
 |-  ( comp ` D ) = ( comp ` D )
9 eqid 
 |-  ( comp ` E ) = ( comp ` E )
10 df-br 
 |-  ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
11 4 10 sylib 
 |-  ( ph -> <. F , G >. e. ( D Func E ) )
12 funcrcl 
 |-  ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
13 11 12 syl 
 |-  ( ph -> ( D e. Cat /\ E e. Cat ) )
14 13 simpld 
 |-  ( ph -> D e. Cat )
15 13 simprd 
 |-  ( ph -> E e. Cat )
16 1 5 2 3 6 7 8 9 14 15 isfunc 
 |-  ( ph -> ( F ( D Func E ) G <-> ( F : B --> ( Base ` E ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
17 4 16 mpbid 
 |-  ( ph -> ( F : B --> ( Base ` E ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) )
18 17 simp2d 
 |-  ( ph -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )