MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfunc Structured version   Visualization version   Unicode version
Theorem isfunc 16524
Description: Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
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 )
Assertion
Ref Expression
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 ) ) ) ) ) )
Distinct variable groups:   m, n, x, y, z, B   D, m, n, x, y, z   m, E, n, x, y, z   m, H, n, x, y, z   m, F, n, x, y, z   m, G, n, x, y, z   x, J, y, z   ph, m, n, x, y, z
Allowed substitution hints:   C( x, y, z, m, n)   .x. ( x, y, z, m, n)   .1. ( x, y, z, m, n)   I( x, y, z, m, n)   J( m, n)   O( x, y, z, m, n)
Proof of Theorem isfunc
Dummy variables b d e f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfunc.d . . . 4 |- ( ph -> D e. Cat )
2 isfunc.e . . . 4 |- ( ph -> E e. Cat )
3 fvexd 6203 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) e. _V )
4 simpl 473 . . . . . . . . 9 |- ( ( d = D /\ e = E ) -> d = D )
54fveq2d 6195 . . . . . . . 8 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = ( Base ` D ) )
6 isfunc.b . . . . . . . 8 |- B = ( Base ` D )
75, 6syl6eqr 2674 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = B )
8 simpr 477 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> b = B )
9 simplr 792 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> e = E )
109fveq2d 6195 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = ( Base ` E ) )
11 isfunc.c . . . . . . . . . . . 12 |- C = ( Base ` E )
1210, 11syl6eqr 2674 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = C )
138, 12feq23d 6040 . . . . . . . . . 10 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f : B --> C ) )
14 fvex 6201 . . . . . . . . . . . 12 |- ( Base ` E ) e. _V
1511, 14eqeltri 2697 . . . . . . . . . . 11 |- C e. _V
16 fvex 6201 . . . . . . . . . . . 12 |- ( Base ` D ) e. _V
176, 16eqeltri 2697 . . . . . . . . . . 11 |- B e. _V
1815, 17elmap 7886 . . . . . . . . . 10 |- ( f e. ( C ^m B ) <-> f : B --> C )
1913, 18syl6bbr 278 . . . . . . . . 9 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f e. ( C ^m B ) ) )
208sqxpeqd 5141 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
2120ixpeq1d 7920 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) = X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) )
229fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = ( Hom ` E ) )
23 isfunc.j . . . . . . . . . . . . . . 15 |- J = ( Hom ` E )
2422, 23syl6eqr 2674 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = J )
2524oveqd 6667 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) = ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) )
26 simpll 790 . . . . . . . . . . . . . . . 16 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> d = D )
2726fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = ( Hom ` D ) )
28 isfunc.h . . . . . . . . . . . . . . 15 |- H = ( Hom ` D )
2927, 28syl6eqr 2674 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = H )
3029fveq1d 6193 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Hom ` d ) ` z ) = ( H ` z ) )
3125, 30oveq12d 6668 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) = ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
3231ixpeq2dv 7924 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) = X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
3321, 32eqtrd 2656 . . . . . . . . . 10 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) = X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
3433eleq2d 2687 . . . . . . . . 9 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) <-> g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
3526fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = ( Id ` D ) )
36 isfunc.1 . . . . . . . . . . . . . . 15 |- .1. = ( Id ` D )
3735, 36syl6eqr 2674 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = .1. )
3837fveq1d 6193 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` d ) ` x ) = ( .1. ` x ) )
3938fveq2d 6195 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( x g x ) ` ( .1. ` x ) ) )
409fveq2d 6195 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = ( Id ` E ) )
41 isfunc.i . . . . . . . . . . . . . 14 |- I = ( Id ` E )
4240, 41syl6eqr 2674 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = I )
4342fveq1d 6193 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` e ) ` ( f ` x ) ) = ( I ` ( f ` x ) ) )
4439, 43eqeq12d 2637 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( Id ` e ) ` ( f ` x ) ) <-> ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) ) )
4529oveqd 6667 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( x ( Hom ` d ) y ) = ( x H y ) )
4629oveqd 6667 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( y ( Hom ` d ) z ) = ( y H z ) )
4726fveq2d 6195 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = (comp ` D ) )
48 isfunc.x . . . . . . . . . . . . . . . . . . . 20 |- .x. = (comp ` D )
4947, 48syl6eqr 2674 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = .x. )
5049oveqd 6667 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. x , y >. (comp ` d ) z ) = ( <. x , y >. .x. z ) )
5150oveqd 6667 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( n ( <. x , y >. (comp ` d ) z ) m ) = ( n ( <. x , y >. .x. z ) m ) )
5251fveq2d 6195 . . . . . . . . . . . . . . . 16 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( x g z ) ` ( n ( <. x , y >. (comp ` d ) z ) m ) ) = ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) )
539fveq2d 6195 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = (comp ` E ) )
54 isfunc.o . . . . . . . . . . . . . . . . . . 19 |- O = (comp ` E )
5553, 54syl6eqr 2674 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = O )
5655oveqd 6667 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. ( f ` x ) , ( f ` y ) >. (comp ` e ) ( f ` z ) ) = ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) )
5756oveqd 6667 . . . . . . . . . . . . . . . 16 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. (comp ` e ) ( f ` z ) ) ( ( x g y ) ` m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) ( ( x g y ) ` m ) ) )
5852, 57eqeq12d 2637 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( ( 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 ) ) <-> ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) ( ( x g y ) ` m ) ) ) )
5946, 58raleqbidv 3152 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( A. n e. ( y ( Hom ` d ) 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 ) ) <-> 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 ) ) ) )
6045, 59raleqbidv 3152 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( A. m e. ( x ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) <-> 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 ) ) ) )
618, 60raleqbidv 3152 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( A. z e. b A. m e. ( x ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) <-> 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 ) ) ) )
628, 61raleqbidv 3152 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( A. y e. b A. z e. b A. m e. ( x ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) <-> 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 ) ) ) )
6344, 62anbi12d 747 . . . . . . . . . 10 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( Id ` e ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) <-> ( ( ( 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 ) ) ) ) )
648, 63raleqbidv 3152 . . . . . . . . 9 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( 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 ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) <-> 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 ) ) ) ) )
6519, 34, 643anbi123d 1399 . . . . . . . 8 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f : b --> ( Base ` e ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` 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 ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) ) <-> ( f e. ( C ^m B ) /\ 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 ) ) ) ) ) )
66 df-3an 1039 . . . . . . . 8 |- ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) <-> ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) )
6765, 66syl6bb 276 . . . . . . 7 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f : b --> ( Base ` e ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` 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 ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) ) <-> ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) ) )
683, 7, 67sbcied2 3473 . . . . . 6 |- ( ( d = D /\ e = E ) -> ( [. ( Base ` d ) / b ]. ( f : b --> ( Base ` e ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` 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 ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) ) <-> ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) ) )
6968opabbidv 4716 . . . . 5 |- ( ( d = D /\ e = E ) -> { <. f , g >. | [. ( Base ` d ) / b ]. ( f : b --> ( Base ` e ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` 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 ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) ) } = { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } )
70 df-func 16518 . . . . 5 |- Func = ( d e. Cat , e e. Cat |-> { <. f , g >. | [. ( Base ` d ) / b ]. ( f : b --> ( Base ` e ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` 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 ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) 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 ) ) ) ) } )
71 ovex 6678 . . . . . . 7 |- ( C ^m B ) e. _V
72 snex 4908 . . . . . . . 8 |- { f } e. _V
73 ovex 6678 . . . . . . . . . 10 |- ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
7473rgenw 2924 . . . . . . . . 9 |- A. z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
75 ixpexg 7932 . . . . . . . . 9 |- ( A. z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V -> X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V )
7674, 75ax-mp 5 . . . . . . . 8 |- X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
7772, 76xpex 6962 . . . . . . 7 |- ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) e. _V
7871, 77iunex 7147 . . . . . 6 |- U_ f e. ( C ^m B ) ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) e. _V
79 simpl 473 . . . . . . . . . 10 |- ( ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) -> ( f e. ( C ^m B ) /\ g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
8079anim2i 593 . . . . . . . . 9 |- ( ( d = <. f , g >. /\ ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) ) -> ( d = <. f , g >. /\ ( f e. ( C ^m B ) /\ g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) ) )
81802eximi 1763 . . . . . . . 8 |- ( E. f E. g ( d = <. f , g >. /\ ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) ) -> E. f E. g ( d = <. f , g >. /\ ( f e. ( C ^m B ) /\ g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) ) )
82 elopab 4983 . . . . . . . 8 |- ( d e. { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } <-> E. f E. g ( d = <. f , g >. /\ ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) ) )
83 eliunxp 5259 . . . . . . . 8 |- ( d e. U_ f e. ( C ^m B ) ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) <-> E. f E. g ( d = <. f , g >. /\ ( f e. ( C ^m B ) /\ g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) ) )
8481, 82, 833imtr4i 281 . . . . . . 7 |- ( d e. { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } -> d e. U_ f e. ( C ^m B ) ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
8584ssriv 3607 . . . . . 6 |- { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } C_ U_ f e. ( C ^m B ) ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
8678, 85ssexi 4803 . . . . 5 |- { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } e. _V
8769, 70, 86ovmpt2a 6791 . . . 4 |- ( ( D e. Cat /\ E e. Cat ) -> ( D Func E ) = { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } )
881, 2, 87syl2anc 693 . . 3 |- ( ph -> ( D Func E ) = { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } )
8988breqd 4664 . 2 |- ( ph -> ( F ( D Func E ) G <-> F { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } G ) )
90 brabv 6699 . . . 4 |- ( F { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } G -> ( F e. _V /\ G e. _V ) )
91 elex 3212 . . . . . 6 |- ( F e. ( C ^m B ) -> F e. _V )
92 elex 3212 . . . . . 6 |- ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) -> G e. _V )
9391, 92anim12i 590 . . . . 5 |- ( ( F e. ( C ^m B ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) -> ( F e. _V /\ G e. _V ) )
94933adant3 1081 . . . 4 |- ( ( F e. ( C ^m B ) /\ 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 ) ) ) ) -> ( F e. _V /\ G e. _V ) )
95 simpl 473 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> f = F )
9695eleq1d 2686 . . . . . . 7 |- ( ( f = F /\ g = G ) -> ( f e. ( C ^m B ) <-> F e. ( C ^m B ) ) )
97 simpr 477 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> g = G )
9895fveq1d 6193 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 1st ` z ) ) = ( F ` ( 1st ` z ) ) )
9995fveq1d 6193 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 2nd ` z ) ) = ( F ` ( 2nd ` z ) ) )
10098, 99oveq12d 6668 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) = ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) )
101100oveq1d 6665 . . . . . . . . 9 |- ( ( f = F /\ g = G ) -> ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
102101ixpeq2dv 7924 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
10397, 102eleq12d 2695 . . . . . . 7 |- ( ( f = F /\ g = G ) -> ( g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
10497oveqd 6667 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( x g x ) = ( x G x ) )
105104fveq1d 6193 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( x g x ) ` ( .1. ` x ) ) = ( ( x G x ) ` ( .1. ` x ) ) )
10695fveq1d 6193 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
107106fveq2d 6195 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( I ` ( f ` x ) ) = ( I ` ( F ` x ) ) )
108105, 107eqeq12d 2637 . . . . . . . . 9 |- ( ( f = F /\ g = G ) -> ( ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) <-> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) )
10997oveqd 6667 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( x g z ) = ( x G z ) )
110109fveq1d 6193 . . . . . . . . . . . 12 |- ( ( f = F /\ g = G ) -> ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) )
11195fveq1d 6193 . . . . . . . . . . . . . . 15 |- ( ( f = F /\ g = G ) -> ( f ` y ) = ( F ` y ) )
112106, 111opeq12d 4410 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> <. ( f ` x ) , ( f ` y ) >. = <. ( F ` x ) , ( F ` y ) >. )
11395fveq1d 6193 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( f ` z ) = ( F ` z ) )
114112, 113oveq12d 6668 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) = ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) )
11597oveqd 6667 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( y g z ) = ( y G z ) )
116115fveq1d 6193 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( y g z ) ` n ) = ( ( y G z ) ` n ) )
11797oveqd 6667 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
118117fveq1d 6193 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( x g y ) ` m ) = ( ( x G y ) ` m ) )
119114, 116, 118oveq123d 6671 . . . . . . . . . . . 12 |- ( ( f = F /\ g = G ) -> ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) ( ( x g y ) ` m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) )
120110, 119eqeq12d 2637 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) ( ( x g y ) ` m ) ) <-> ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) ( ( x G y ) ` m ) ) ) )
1211202ralbidv 2989 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( 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 ) ) <-> 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 ) ) ) )
1221212ralbidv 2989 . . . . . . . . 9 |- ( ( f = F /\ g = G ) -> ( 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 ) ) <-> 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 ) ) ) )
123108, 122anbi12d 747 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> ( ( ( ( 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 ) ) ) <-> ( ( ( 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 ) ) ) ) )
124123ralbidv 2986 . . . . . . 7 |- ( ( f = F /\ g = G ) -> ( 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 ) ) ) <-> 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 ) ) ) ) )
12596, 103, 1243anbi123d 1399 . . . . . 6 |- ( ( f = F /\ g = G ) -> ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) <-> ( F e. ( C ^m B ) /\ 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 ) ) ) ) ) )
12666, 125syl5bbr 274 . . . . 5 |- ( ( f = F /\ g = G ) -> ( ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) <-> ( F e. ( C ^m B ) /\ 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 ) ) ) ) ) )
127 eqid 2622 . . . . 5 |- { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } = { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) }
128126, 127brabga 4989 . . . 4 |- ( ( F e. _V /\ G e. _V ) -> ( F { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } G <-> ( F e. ( C ^m B ) /\ 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 ) ) ) ) ) )
12990, 94, 128pm5.21nii 368 . . 3 |- ( F { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } G <-> ( F e. ( C ^m B ) /\ 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 ) ) ) ) )
13015, 17elmap 7886 . . . 4 |- ( F e. ( C ^m B ) <-> F : B --> C )
1311303anbi1i 1253 . . 3 |- ( ( F e. ( C ^m B ) /\ 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 ) ) ) ) <-> ( 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 ) ) ) ) )
132129, 131bitri 264 . 2 |- ( F { <. f , g >. | ( ( f e. ( C ^m B ) /\ 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 ) ) ) ) } 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 ) ) ) ) )
13389, 132syl6bb 276 1 |- ( 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 ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   _Vcvv 3200   [.wsbc 3435   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   {copab 4712   X. cxp 5112   -->wf 5884   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   X_cixp 7908   Basecbs 15857   Hom chom 15952  compcco 15953   Catccat 16325   Idccid 16326   Func cfunc 16514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859  df-ixp 7909  df-func 16518
This theorem is referenced by:  isfuncd  16525  funcf1  16526  funcixp  16527  funcid  16530  funcco  16531  idfucl  16541  cofucl  16548  funcres2b  16557  funcpropd  16560
  Copyright terms: Public domain W3C validator