MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfunc Structured version   Unicode version
Theorem isfunc 14789
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 fvex 5716 . . . . . . . 8 |- ( Base ` d ) e. _V
43a1i 11 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) e. _V )
5 simpl 457 . . . . . . . . 9 |- ( ( d = D /\ e = E ) -> d = D )
65fveq2d 5710 . . . . . . . 8 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = ( Base ` D ) )
7 isfunc.b . . . . . . . 8 |- B = ( Base ` D )
86, 7syl6eqr 2493 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = B )
9 simpr 461 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> b = B )
10 simplr 754 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> e = E )
1110fveq2d 5710 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = ( Base ` E ) )
12 isfunc.c . . . . . . . . . . . 12 |- C = ( Base ` E )
1311, 12syl6eqr 2493 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = C )
149, 13feq23d 5569 . . . . . . . . . 10 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f : B --> C ) )
15 fvex 5716 . . . . . . . . . . . 12 |- ( Base ` E ) e. _V
1612, 15eqeltri 2513 . . . . . . . . . . 11 |- C e. _V
17 fvex 5716 . . . . . . . . . . . 12 |- ( Base ` D ) e. _V
187, 17eqeltri 2513 . . . . . . . . . . 11 |- B e. _V
1916, 18elmap 7256 . . . . . . . . . 10 |- ( f e. ( C ^m B ) <-> f : B --> C )
2014, 19syl6bbr 263 . . . . . . . . 9 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f e. ( C ^m B ) ) )
219, 9xpeq12d 4880 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
2221ixpeq1d 7290 . . . . . . . . . . 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 ) ) )
2310fveq2d 5710 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = ( Hom ` E ) )
24 isfunc.j . . . . . . . . . . . . . . 15 |- J = ( Hom ` E )
2523, 24syl6eqr 2493 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = J )
2625oveqd 6123 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) = ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) )
27 simpll 753 . . . . . . . . . . . . . . . 16 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> d = D )
2827fveq2d 5710 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = ( Hom ` D ) )
29 isfunc.h . . . . . . . . . . . . . . 15 |- H = ( Hom ` D )
3028, 29syl6eqr 2493 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = H )
3130fveq1d 5708 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Hom ` d ) ` z ) = ( H ` z ) )
3226, 31oveq12d 6124 . . . . . . . . . . . 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 ) ) )
3332ixpeq2dv 7294 . . . . . . . . . . 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 ) ) )
3422, 33eqtrd 2475 . . . . . . . . . 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 ) ) )
3534eleq2d 2510 . . . . . . . . 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 ) ) ) )
3627fveq2d 5710 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = ( Id ` D ) )
37 isfunc.1 . . . . . . . . . . . . . . 15 |- .1. = ( Id ` D )
3836, 37syl6eqr 2493 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = .1. )
3938fveq1d 5708 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` d ) ` x ) = ( .1. ` x ) )
4039fveq2d 5710 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( x g x ) ` ( .1. ` x ) ) )
4110fveq2d 5710 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = ( Id ` E ) )
42 isfunc.i . . . . . . . . . . . . . 14 |- I = ( Id ` E )
4341, 42syl6eqr 2493 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = I )
4443fveq1d 5708 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` e ) ` ( f ` x ) ) = ( I ` ( f ` x ) ) )
4540, 44eqeq12d 2457 . . . . . . . . . . 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 ) ) ) )
4630oveqd 6123 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( x ( Hom ` d ) y ) = ( x H y ) )
4730oveqd 6123 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( y ( Hom ` d ) z ) = ( y H z ) )
4827fveq2d 5710 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = (comp ` D ) )
49 isfunc.x . . . . . . . . . . . . . . . . . . . 20 |- .x. = (comp ` D )
5048, 49syl6eqr 2493 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = .x. )
5150oveqd 6123 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. x , y >. (comp ` d ) z ) = ( <. x , y >. .x. z ) )
5251oveqd 6123 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( n ( <. x , y >. (comp ` d ) z ) m ) = ( n ( <. x , y >. .x. z ) m ) )
5352fveq2d 5710 . . . . . . . . . . . . . . . 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 ) ) )
5410fveq2d 5710 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = (comp ` E ) )
55 isfunc.o . . . . . . . . . . . . . . . . . . 19 |- O = (comp ` E )
5654, 55syl6eqr 2493 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = O )
5756oveqd 6123 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. ( f ` x ) , ( f ` y ) >. (comp ` e ) ( f ` z ) ) = ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) )
5857oveqd 6123 . . . . . . . . . . . . . . . 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 ) ) )
5953, 58eqeq12d 2457 . . . . . . . . . . . . . . 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 ) ) ) )
6047, 59raleqbidv 2946 . . . . . . . . . . . . . 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 ) ) ) )
6146, 60raleqbidv 2946 . . . . . . . . . . . . 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 ) ) ) )
629, 61raleqbidv 2946 . . . . . . . . . . . 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 ) ) ) )
639, 62raleqbidv 2946 . . . . . . . . . . 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 ) ) ) )
6445, 63anbi12d 710 . . . . . . . . . 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 ) ) ) ) )
659, 64raleqbidv 2946 . . . . . . . . 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 ) ) ) ) )
6620, 35, 653anbi123d 1289 . . . . . . . 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 ) ) ) ) ) )
67 df-3an 967 . . . . . . . 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 ) ) ) ) )
6866, 67syl6bb 261 . . . . . . 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 ) ) ) ) ) )
694, 8, 68sbcied2 3239 . . . . . 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 ) ) ) ) ) )
7069opabbidv 4370 . . . . 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 ) ) ) ) } )
71 df-func 14783 . . . . 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 ) ) ) ) } )
72 ovex 6131 . . . . . . 7 |- ( C ^m B ) e. _V
73 snex 4548 . . . . . . . 8 |- { f } e. _V
74 ovex 6131 . . . . . . . . . 10 |- ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
7574rgenw 2798 . . . . . . . . 9 |- A. z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
76 ixpexg 7302 . . . . . . . . 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 )
7775, 76ax-mp 5 . . . . . . . 8 |- X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
7873, 77xpex 6523 . . . . . . 7 |- ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) e. _V
7972, 78iunex 6572 . . . . . 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
80 simpl 457 . . . . . . . . . 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 ) ) ) )
8180anim2i 569 . . . . . . . . 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 ) ) ) ) )
82812eximi 1626 . . . . . . . 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 ) ) ) ) )
83 elopab 4612 . . . . . . . 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 ) ) ) ) ) )
84 eliunxp 4992 . . . . . . . 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 ) ) ) ) )
8582, 83, 843imtr4i 266 . . . . . . 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 ) ) ) )
8685ssriv 3375 . . . . . 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 ) ) )
8779, 86ssexi 4452 . . . . 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
8870, 71, 87ovmpt2a 6236 . . . 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 ) ) ) ) } )
891, 2, 88syl2anc 661 . . 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 ) ) ) ) } )
9089breqd 4318 . 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 ) )
91 brabv 6147 . . . 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 ) )
92 elex 2996 . . . . . 6 |- ( F e. ( C ^m B ) -> F e. _V )
93 elex 2996 . . . . . 6 |- ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) -> G e. _V )
9492, 93anim12i 566 . . . . 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 ) )
95943adant3 1008 . . . 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 ) )
96 simpl 457 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> f = F )
9796eleq1d 2509 . . . . . . 7 |- ( ( f = F /\ g = G ) -> ( f e. ( C ^m B ) <-> F e. ( C ^m B ) ) )
98 simpr 461 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> g = G )
9996fveq1d 5708 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 1st ` z ) ) = ( F ` ( 1st ` z ) ) )
10096fveq1d 5708 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 2nd ` z ) ) = ( F ` ( 2nd ` z ) ) )
10199, 100oveq12d 6124 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) = ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) )
102101oveq1d 6121 . . . . . . . . 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 ) ) )
103102ixpeq2dv 7294 . . . . . . . 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 ) ) )
10498, 103eleq12d 2511 . . . . . . 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 ) ) ) )
10598oveqd 6123 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( x g x ) = ( x G x ) )
106105fveq1d 5708 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( x g x ) ` ( .1. ` x ) ) = ( ( x G x ) ` ( .1. ` x ) ) )
10796fveq1d 5708 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
108107fveq2d 5710 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( I ` ( f ` x ) ) = ( I ` ( F ` x ) ) )
109106, 108eqeq12d 2457 . . . . . . . . 9 |- ( ( f = F /\ g = G ) -> ( ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) <-> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) )
11098oveqd 6123 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( x g z ) = ( x G z ) )
111110fveq1d 5708 . . . . . . . . . . . 12 |- ( ( f = F /\ g = G ) -> ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) )
11296fveq1d 5708 . . . . . . . . . . . . . . 15 |- ( ( f = F /\ g = G ) -> ( f ` y ) = ( F ` y ) )
113107, 112opeq12d 4082 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> <. ( f ` x ) , ( f ` y ) >. = <. ( F ` x ) , ( F ` y ) >. )
11496fveq1d 5708 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( f ` z ) = ( F ` z ) )
115113, 114oveq12d 6124 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) = ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) )
11698oveqd 6123 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( y g z ) = ( y G z ) )
117116fveq1d 5708 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( y g z ) ` n ) = ( ( y G z ) ` n ) )
11898oveqd 6123 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
119118fveq1d 5708 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( x g y ) ` m ) = ( ( x G y ) ` m ) )
120115, 117, 119oveq123d 6127 . . . . . . . . . . . 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 ) ) )
121111, 120eqeq12d 2457 . . . . . . . . . . 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 ) ) ) )
1221212ralbidv 2772 . . . . . . . . . 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 ) ) ) )
1231222ralbidv 2772 . . . . . . . . 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 ) ) ) )
124109, 123anbi12d 710 . . . . . . . 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 ) ) ) ) )
125124ralbidv 2750 . . . . . . 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 ) ) ) ) )
12697, 104, 1253anbi123d 1289 . . . . . 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 ) ) ) ) ) )
12767, 126syl5bbr 259 . . . . 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 ) ) ) ) ) )
128 eqid 2443 . . . . 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 ) ) ) ) }
129127, 128brabga 4618 . . . 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 ) ) ) ) ) )
13091, 95, 129pm5.21nii 353 . . 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 ) ) ) ) )
13116, 18elmap 7256 . . . 4 |- ( F e. ( C ^m B ) <-> F : B --> C )
1321313anbi1i 1178 . . 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 ) ) ) ) )
133130, 132bitri 249 . 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 ) ) ) ) )
13490, 133syl6bb 261 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 184   /\ wa 369   /\ w3a 965   = wceq 1369   E.wex 1586   e. wcel 1756   A.wral 2730   _Vcvv 2987   [.wsbc 3201   {csn 3892   <.cop 3898   U_ciun 4186   class class class wbr 4307   {copab 4364   X. cxp 4853   -->wf 5429   ` cfv 5433  (class class class)co 6106   1stc1st 6590   2ndc2nd 6591   ^m cmap 7229   X_cixp 7278   Basecbs 14189   Hom chom 14264  compcco 14265   Catccat 14617   Idccid 14618   Func cfunc 14779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-reu 2737  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-map 7231  df-ixp 7279  df-func 14783
This theorem is referenced by:  isfuncd  14790  funcf1  14791  funcixp  14792  funcid  14795  funcco  14796  idfucl  14806  cofucl  14813  funcres2b  14822  funcpropd  14825
  Copyright terms: Public domain W3C validator