MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfunc Structured version   Visualization version   Unicode version
Theorem isfunc 15824
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 5902 . . . . . . . 8 |- ( Base ` d ) e. _V
43a1i 11 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) e. _V )
5 simpl 463 . . . . . . . . 9 |- ( ( d = D /\ e = E ) -> d = D )
65fveq2d 5896 . . . . . . . 8 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = ( Base ` D ) )
7 isfunc.b . . . . . . . 8 |- B = ( Base ` D )
86, 7syl6eqr 2514 . . . . . . 7 |- ( ( d = D /\ e = E ) -> ( Base ` d ) = B )
9 simpr 467 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> b = B )
10 simplr 767 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> e = E )
1110fveq2d 5896 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = ( Base ` E ) )
12 isfunc.c . . . . . . . . . . . 12 |- C = ( Base ` E )
1311, 12syl6eqr 2514 . . . . . . . . . . 11 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = C )
149, 13feq23d 5750 . . . . . . . . . 10 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f : B --> C ) )
15 fvex 5902 . . . . . . . . . . . 12 |- ( Base ` E ) e. _V
1612, 15eqeltri 2536 . . . . . . . . . . 11 |- C e. _V
17 fvex 5902 . . . . . . . . . . . 12 |- ( Base ` D ) e. _V
187, 17eqeltri 2536 . . . . . . . . . . 11 |- B e. _V
1916, 18elmap 7531 . . . . . . . . . 10 |- ( f e. ( C ^m B ) <-> f : B --> C )
2014, 19syl6bbr 271 . . . . . . . . 9 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f e. ( C ^m B ) ) )
219sqxpeqd 4882 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
2221ixpeq1d 7565 . . . . . . . . . . 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 5896 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = ( Hom ` E ) )
24 isfunc.j . . . . . . . . . . . . . . 15 |- J = ( Hom ` E )
2523, 24syl6eqr 2514 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = J )
2625oveqd 6337 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) = ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) )
27 simpll 765 . . . . . . . . . . . . . . . 16 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> d = D )
2827fveq2d 5896 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = ( Hom ` D ) )
29 isfunc.h . . . . . . . . . . . . . . 15 |- H = ( Hom ` D )
3028, 29syl6eqr 2514 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = H )
3130fveq1d 5894 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Hom ` d ) ` z ) = ( H ` z ) )
3226, 31oveq12d 6338 . . . . . . . . . . . 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 7569 . . . . . . . . . . 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 2496 . . . . . . . . . 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 2525 . . . . . . . . 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 5896 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = ( Id ` D ) )
37 isfunc.1 . . . . . . . . . . . . . . 15 |- .1. = ( Id ` D )
3836, 37syl6eqr 2514 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = .1. )
3938fveq1d 5894 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` d ) ` x ) = ( .1. ` x ) )
4039fveq2d 5896 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( x g x ) ` ( .1. ` x ) ) )
4110fveq2d 5896 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = ( Id ` E ) )
42 isfunc.i . . . . . . . . . . . . . 14 |- I = ( Id ` E )
4341, 42syl6eqr 2514 . . . . . . . . . . . . 13 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = I )
4443fveq1d 5894 . . . . . . . . . . . 12 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` e ) ` ( f ` x ) ) = ( I ` ( f ` x ) ) )
4540, 44eqeq12d 2477 . . . . . . . . . . 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 6337 . . . . . . . . . . . . . 14 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( x ( Hom ` d ) y ) = ( x H y ) )
4730oveqd 6337 . . . . . . . . . . . . . . 15 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( y ( Hom ` d ) z ) = ( y H z ) )
4827fveq2d 5896 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = (comp ` D ) )
49 isfunc.x . . . . . . . . . . . . . . . . . . . 20 |- .x. = (comp ` D )
5048, 49syl6eqr 2514 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` d ) = .x. )
5150oveqd 6337 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. x , y >. (comp ` d ) z ) = ( <. x , y >. .x. z ) )
5251oveqd 6337 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( n ( <. x , y >. (comp ` d ) z ) m ) = ( n ( <. x , y >. .x. z ) m ) )
5352fveq2d 5896 . . . . . . . . . . . . . . . 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 5896 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = (comp ` E ) )
55 isfunc.o . . . . . . . . . . . . . . . . . . 19 |- O = (comp ` E )
5654, 55syl6eqr 2514 . . . . . . . . . . . . . . . . . 18 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> (comp ` e ) = O )
5756oveqd 6337 . . . . . . . . . . . . . . . . 17 |- ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. ( f ` x ) , ( f ` y ) >. (comp ` e ) ( f ` z ) ) = ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) )
5857oveqd 6337 . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . 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 3013 . . . . . . . . . . . . . 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 3013 . . . . . . . . . . . . 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 3013 . . . . . . . . . . . 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 3013 . . . . . . . . . . 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 722 . . . . . . . . . 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 3013 . . . . . . . . 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 1348 . . . . . . . 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 993 . . . . . . . 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 269 . . . . . . 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 3317 . . . . . 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 4482 . . . . 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 15818 . . . . 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 6348 . . . . . . 7 |- ( C ^m B ) e. _V
73 snex 4658 . . . . . . . 8 |- { f } e. _V
74 ovex 6348 . . . . . . . . . 10 |- ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
7574rgenw 2761 . . . . . . . . 9 |- A. z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
76 ixpexg 7577 . . . . . . . . 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 6627 . . . . . . 7 |- ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) e. _V
7972, 78iunex 6805 . . . . . 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 463 . . . . . . . . . 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 577 . . . . . . . . 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 1719 . . . . . . . 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 4726 . . . . . . . 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 4994 . . . . . . . 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 274 . . . . . . 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 3448 . . . . . 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 4564 . . . . 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 6459 . . . 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 671 . . 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 4429 . 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 6367 . . . 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 3066 . . . . . 6 |- ( F e. ( C ^m B ) -> F e. _V )
93 elex 3066 . . . . . 6 |- ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) -> G e. _V )
9492, 93anim12i 574 . . . . 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 1034 . . . 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 463 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> f = F )
9796eleq1d 2524 . . . . . . 7 |- ( ( f = F /\ g = G ) -> ( f e. ( C ^m B ) <-> F e. ( C ^m B ) ) )
98 simpr 467 . . . . . . . 8 |- ( ( f = F /\ g = G ) -> g = G )
9996fveq1d 5894 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 1st ` z ) ) = ( F ` ( 1st ` z ) ) )
10096fveq1d 5894 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` ( 2nd ` z ) ) = ( F ` ( 2nd ` z ) ) )
10199, 100oveq12d 6338 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) = ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) )
102101oveq1d 6335 . . . . . . . . 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 7569 . . . . . . . 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 2534 . . . . . . 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 6337 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( x g x ) = ( x G x ) )
106105fveq1d 5894 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( ( x g x ) ` ( .1. ` x ) ) = ( ( x G x ) ` ( .1. ` x ) ) )
10796fveq1d 5894 . . . . . . . . . . 11 |- ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
108107fveq2d 5896 . . . . . . . . . 10 |- ( ( f = F /\ g = G ) -> ( I ` ( f ` x ) ) = ( I ` ( F ` x ) ) )
109106, 108eqeq12d 2477 . . . . . . . . 9 |- ( ( f = F /\ g = G ) -> ( ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) <-> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) )
11098oveqd 6337 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( x g z ) = ( x G z ) )
111110fveq1d 5894 . . . . . . . . . . . 12 |- ( ( f = F /\ g = G ) -> ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) )
11296fveq1d 5894 . . . . . . . . . . . . . . 15 |- ( ( f = F /\ g = G ) -> ( f ` y ) = ( F ` y ) )
113107, 112opeq12d 4188 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> <. ( f ` x ) , ( f ` y ) >. = <. ( F ` x ) , ( F ` y ) >. )
11496fveq1d 5894 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( f ` z ) = ( F ` z ) )
115113, 114oveq12d 6338 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) = ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) )
11698oveqd 6337 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( y g z ) = ( y G z ) )
117116fveq1d 5894 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( y g z ) ` n ) = ( ( y G z ) ` n ) )
11898oveqd 6337 . . . . . . . . . . . . . 14 |- ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
119118fveq1d 5894 . . . . . . . . . . . . 13 |- ( ( f = F /\ g = G ) -> ( ( x g y ) ` m ) = ( ( x G y ) ` m ) )
120115, 117, 119oveq123d 6341 . . . . . . . . . . . 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 2477 . . . . . . . . . . 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 2844 . . . . . . . . . 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 2844 . . . . . . . . 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 722 . . . . . . . 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 2839 . . . . . . 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 1348 . . . . . 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 267 . . . . 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 2462 . . . . 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 4732 . . . 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 359 . . 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 7531 . . . 4 |- ( F e. ( C ^m B ) <-> F : B --> C )
1321313anbi1i 1205 . . 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 257 . 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 269 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 189   /\ wa 375   /\ w3a 991   = wceq 1455   E.wex 1674   e. wcel 1898   A.wral 2749   _Vcvv 3057   [.wsbc 3279   {csn 3980   <.cop 3986   U_ciun 4292   class class class wbr 4418   {copab 4476   X. cxp 4854   -->wf 5601   ` cfv 5605  (class class class)co 6320   1stc1st 6823   2ndc2nd 6824   ^m cmap 7503   X_cixp 7553   Basecbs 15176   Hom chom 15256  compcco 15257   Catccat 15625   Idccid 15626   Func cfunc 15814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-map 7505  df-ixp 7554  df-func 15818
This theorem is referenced by:  isfuncd  15825  funcf1  15826  funcixp  15827  funcid  15830  funcco  15831  idfucl  15841  cofucl  15848  funcres2b  15857  funcpropd  15860
  Copyright terms: Public domain W3C validator