MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfunc Structured version   Unicode version
Theorem isfunc 15279
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 5882 . . . . . . . 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 5876 . . . . . . . 8 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = ( Base ` D ) )
7 isfunc.b . . . . . . . 8 |- B = ( Base ` D )
86, 7syl6eqr 2516 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = B )
9 simpr 461 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> b = B )
10 simplr 755 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> e = E )
1110fveq2d 5876 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = ( Base ` E ) )
12 isfunc.c . . . . . . . . . . . 12 |- C = ( Base ` E )
1311, 12syl6eqr 2516 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = C )
149, 13feq23d 5732 . . . . . . . . . 10 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f : B --> C ) )
15 fvex 5882 . . . . . . . . . . . 12 |- ( Base ` E ) e. _V
1612, 15eqeltri 2541 . . . . . . . . . . 11 |- C e. _V
17 fvex 5882 . . . . . . . . . . . 12 |- ( Base ` D ) e. _V
187, 17eqeltri 2541 . . . . . . . . . . 11 |- B e. _V
1916, 18elmap 7466 . . . . . . . . . 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 ) ) )
219sqxpeqd 5034 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
2221ixpeq1d 7500 . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = ( Hom ` E ) )
24 isfunc.j . . . . . . . . . . . . . . 15 |- J = ( Hom ` E )
2523, 24syl6eqr 2516 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = J )
2625oveqd 6313 . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = ( Hom ` D ) )
29 isfunc.h . . . . . . . . . . . . . . 15 |- H = ( Hom ` D )
3028, 29syl6eqr 2516 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = H )
3130fveq1d 5874 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Hom ` d ) ` z ) = ( H ` z ) )
3226, 31oveq12d 6314 . . . . . . . . . . . 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 7504 . . . . . . . . . . 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 2498 . . . . . . . . . 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 2527 . . . . . . . . 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 5876 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = ( Id ` D ) )
37 isfunc.1 . . . . . . . . . . . . . . 15 |- .1. = ( Id ` D )
3836, 37syl6eqr 2516 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = .1. )
3938fveq1d 5874 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` d ) ` x ) = ( .1. ` x ) )
4039fveq2d 5876 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( x g x ) ` ( .1. ` x ) ) )
4110fveq2d 5876 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = ( Id ` E ) )
42 isfunc.i . . . . . . . . . . . . . 14 |- I = ( Id ` E )
4341, 42syl6eqr 2516 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = I )
4443fveq1d 5874 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` e ) ` ( f ` x ) ) = ( I ` ( f ` x ) ) )
4540, 44eqeq12d 2479 . . . . . . . . . . 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 6313 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( x ( Hom ` d ) y ) = ( x H y ) )
4730oveqd 6313 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( y ( Hom ` d ) z ) = ( y H z ) )
4827fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = (comp ` D ) )
49 isfunc.x . . . . . . . . . . . . . . . . . . . 20 |- .x. = (comp ` D )
5048, 49syl6eqr 2516 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = .x. )
5150oveqd 6313 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. x , y >. (comp ` d ) z ) = ( <. x , y >. .x. z ) )
5251oveqd 6313 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( n ( <. x , y >. (comp ` d ) z ) m ) = ( n ( <. x , y >. .x. z ) m ) )
5352fveq2d 5876 . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = (comp ` E ) )
55 isfunc.o . . . . . . . . . . . . . . . . . . 19 |- O = (comp ` E )
5654, 55syl6eqr 2516 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = O )
5756oveqd 6313 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. ( f ` x ) , ( f ` y ) >. (comp ` e ) ( f ` z ) ) = ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) )
5857oveqd 6313 . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . 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 3068 . . . . . . . . . . . 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 3068 . . . . . . . . . . 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 3068 . . . . . . . . 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 1299 . . . . . . . 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 975 . . . . . . . 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 3365 . . . . . 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 4520 . . . . 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 15273 . . . . 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 6324 . . . . . . 7 |- ( C ^m B ) e. _V
73 snex 4697 . . . . . . . 8 |- { f } e. _V
74 ovex 6324 . . . . . . . . . 10 |- ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
7574rgenw 2818 . . . . . . . . 9 |- A. z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
76 ixpexg 7512 . . . . . . . . 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 6603 . . . . . . 7 |- ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) e. _V
7972, 78iunex 6779 . . . . . 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 1658 . . . . . . . 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 4764 . . . . . . . 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 5150 . . . . . . . 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 3503 . . . . . 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 4601 . . . . 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 6432 . . . 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 4467 . 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 6341 . . . 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 3118 . . . . . 6 |- ( F e. ( C ^m B ) -> F e. _V )
93 elex 3118 . . . . . 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 1016 . . . 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 2526 . . . . . . 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 5874 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 1st ` z ) ) = ( F ` ( 1st ` z ) ) )
10096fveq1d 5874 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 2nd ` z ) ) = ( F ` ( 2nd ` z ) ) )
10199, 100oveq12d 6314 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) = ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) )
102101oveq1d 6311 . . . . . . . . 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 7504 . . . . . . . 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 2539 . . . . . . 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 6313 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( x g x ) = ( x G x ) )
106105fveq1d 5874 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( x g x ) ` ( .1. ` x ) ) = ( ( x G x ) ` ( .1. ` x ) ) )
10796fveq1d 5874 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
108107fveq2d 5876 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( I ` ( f ` x ) ) = ( I ` ( F ` x ) ) )
109106, 108eqeq12d 2479 . . . . . . . . 9 |- ( ( f = F /\ g = G ) -> ( ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) <-> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) )
11098oveqd 6313 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( x g z ) = ( x G z ) )
111110fveq1d 5874 . . . . . . . . . . . 12 |- ( ( f = F /\ g = G ) -> ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) )
11296fveq1d 5874 . . . . . . . . . . . . . . 15 |- ( ( f = F /\ g = G ) -> ( f ` y ) = ( F ` y ) )
113107, 112opeq12d 4227 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> <. ( f ` x ) , ( f ` y ) >. = <. ( F ` x ) , ( F ` y ) >. )
11496fveq1d 5874 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( f ` z ) = ( F ` z ) )
115113, 114oveq12d 6314 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) = ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) )
11698oveqd 6313 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( y g z ) = ( y G z ) )
117116fveq1d 5874 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( y g z ) ` n ) = ( ( y G z ) ` n ) )
11898oveqd 6313 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
119118fveq1d 5874 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( x g y ) ` m ) = ( ( x G y ) ` m ) )
120115, 117, 119oveq123d 6317 . . . . . . . . . . . 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 2479 . . . . . . . . . . 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 2901 . . . . . . . . . 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 2901 . . . . . . . . 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 2896 . . . . . . 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 1299 . . . . . 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 2457 . . . . 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 4770 . . . 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 7466 . . . 4 |- ( F e. ( C ^m B ) <-> F : B --> C )
1321313anbi1i 1187 . . 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 973   = wceq 1395   E.wex 1613   e. wcel 1819   A.wral 2807   _Vcvv 3109   [.wsbc 3327   {csn 4032   <.cop 4038   U_ciun 4332   class class class wbr 4456   {copab 4514   X. cxp 5006   -->wf 5590   ` cfv 5594  (class class class)co 6296   1stc1st 6797   2ndc2nd 6798   ^m cmap 7438   X_cixp 7488   Basecbs 14643   Hom chom 14722  compcco 14723   Catccat 15080   Idccid 15081   Func cfunc 15269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-map 7440  df-ixp 7489  df-func 15273
This theorem is referenced by:  isfuncd  15280  funcf1  15281  funcixp  15282  funcid  15285  funcco  15286  idfucl  15296  cofucl  15303  funcres2b  15312  funcpropd  15315
  Copyright terms: Public domain W3C validator