Metamath Proof Explorer

Theorem isfuncd

Description: Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses isfunc.b 
|- B = ( Base ` D )
isfunc.c 
|- C = ( Base ` E )
isfunc.h 
|- H = ( Hom ` D )
isfunc.j 
|- J = ( Hom ` E )
isfunc.1 
|- .1. = ( Id ` D )
isfunc.i 
|- I = ( Id ` E )
isfunc.x 
|- .x. = ( comp ` D )
isfunc.o 
|- O = ( comp ` E )
isfunc.d 
|- ( ph -> D e. Cat )
isfunc.e 
|- ( ph -> E e. Cat )
isfuncd.1 
|- ( ph -> F : B --> C )
isfuncd.2 
|- ( ph -> G Fn ( B X. B ) )
isfuncd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
isfuncd.4 
|- ( ( ph /\ x e. B ) -> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) )
isfuncd.5 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )
Assertion isfuncd 
|- ( ph -> F ( D Func E ) G )

Proof

Step Hyp Ref Expression
1 isfunc.b 
 |-  B = ( Base ` D )
2 isfunc.c 
 |-  C = ( Base ` E )
3 isfunc.h 
 |-  H = ( Hom ` D )
4 isfunc.j 
 |-  J = ( Hom ` E )
5 isfunc.1 
 |-  .1. = ( Id ` D )
6 isfunc.i 
 |-  I = ( Id ` E )
7 isfunc.x 
 |-  .x. = ( comp ` D )
8 isfunc.o 
 |-  O = ( comp ` E )
9 isfunc.d 
 |-  ( ph -> D e. Cat )
10 isfunc.e 
 |-  ( ph -> E e. Cat )
11 isfuncd.1 
 |-  ( ph -> F : B --> C )
12 isfuncd.2 
 |-  ( ph -> G Fn ( B X. B ) )
13 isfuncd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
14 isfuncd.4 
 |-  ( ( ph /\ x e. B ) -> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) )
15 isfuncd.5 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )
16 1 fvexi 
 |-  B e. _V
17 16 16 xpex 
 |-  ( B X. B ) e. _V
18 fnex 
 |-  ( ( G Fn ( B X. B ) /\ ( B X. B ) e. _V ) -> G e. _V )
19 12 17 18 sylancl 
 |-  ( ph -> G e. _V )
20 ovex 
 |-  ( ( F ` x ) J ( F ` y ) ) e. _V
21 ovex 
 |-  ( x H y ) e. _V
22 20 21 elmap 
 |-  ( ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
23 13 22 sylibr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) )
24 23 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) )
25 fveq2 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( G ` <. x , y >. ) )
26 df-ov 
 |-  ( x G y ) = ( G ` <. x , y >. )
27 25 26 eqtr4di 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( x G y ) )
28 vex 
 |-  x e. _V
29 vex 
 |-  y e. _V
30 28 29 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
31 30 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 1st ` z ) ) = ( F ` x ) )
32 28 29 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
33 32 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 2nd ` z ) ) = ( F ` y ) )
34 31 33 oveq12d 
 |-  ( z = <. x , y >. -> ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) = ( ( F ` x ) J ( F ` y ) ) )
35 fveq2 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( H ` <. x , y >. ) )
36 df-ov 
 |-  ( x H y ) = ( H ` <. x , y >. )
37 35 36 eqtr4di 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( x H y ) )
38 34 37 oveq12d 
 |-  ( z = <. x , y >. -> ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) )
39 27 38 eleq12d 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) ) )
40 39 ralxp 
 |-  ( A. z e. ( B X. B ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> A. x e. B A. y e. B ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) )
41 24 40 sylibr 
 |-  ( ph -> A. z e. ( B X. B ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
42 elixp2 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. ( B X. B ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
43 19 12 41 42 syl3anbrc 
 |-  ( ph -> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
44 15 3expia 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( m e. ( x H y ) /\ n e. ( y H z ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
45 44 3exp2 
 |-  ( ph -> ( x e. B -> ( y e. B -> ( z e. B -> ( ( m e. ( x H y ) /\ n e. ( y H z ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) ) )
46 45 imp43 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( ( m e. ( x H y ) /\ n e. ( y H z ) ) -> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
47 46 ralrimivv 
 |-  ( ( ( ph /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> A. m e. ( x H y ) A. n e. ( y H z ) ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )
48 47 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> 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 >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )
49 14 48 jca 
 |-  ( ( ph /\ x e. B ) -> ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( 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 >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
50 49 ralrimiva 
 |-  ( ph -> A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( 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 >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
51 1 2 3 4 5 6 7 8 9 10 isfunc 
 |-  ( ph -> ( F ( D Func E ) G <-> ( F : B --> C /\ 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 ) ` ( .1. ` x ) ) = ( I ` ( 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 >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
52 11 43 50 51 mpbir3and 
 |-  ( ph -> F ( D Func E ) G )