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 )