Metamath Proof Explorer

Theorem isfunc

Description: Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isfunc.b 
|- B = ( Base ` D )
isfunc.c 
|- C = ( Base ` E )
isfunc.h 
|- H = ( Hom ` D )
isfunc.j 
|- J = ( Hom ` E )
isfunc.1 
|- .1. = ( Id ` D )
isfunc.i 
|- I = ( Id ` E )
isfunc.x 
|- .x. = ( comp ` D )
isfunc.o 
|- O = ( comp ` E )
isfunc.d 
|- ( ph -> D e. Cat )
isfunc.e 
|- ( ph -> E e. Cat )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isfunc.b 
 |-  B = ( Base ` D )
2 isfunc.c 
 |-  C = ( Base ` E )
3 isfunc.h 
 |-  H = ( Hom ` D )
4 isfunc.j 
 |-  J = ( Hom ` E )
5 isfunc.1 
 |-  .1. = ( Id ` D )
6 isfunc.i 
 |-  I = ( Id ` E )
7 isfunc.x 
 |-  .x. = ( comp ` D )
8 isfunc.o 
 |-  O = ( comp ` E )
9 isfunc.d 
 |-  ( ph -> D e. Cat )
10 isfunc.e 
 |-  ( ph -> E e. Cat )
11 fvexd 
 |-  ( ( d = D /\ e = E ) -> ( Base ` d ) e. _V )
12 simpl 
 |-  ( ( d = D /\ e = E ) -> d = D )
13 12 fveq2d 
 |-  ( ( d = D /\ e = E ) -> ( Base ` d ) = ( Base ` D ) )
14 13 1 eqtr4di 
 |-  ( ( d = D /\ e = E ) -> ( Base ` d ) = B )
15 simpr 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> b = B )
16 simplr 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> e = E )
17 16 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = ( Base ` E ) )
18 17 2 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Base ` e ) = C )
19 15 18 feq23d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f : B --> C ) )
20 2 fvexi 
 |-  C e. _V
21 1 fvexi 
 |-  B e. _V
22 20 21 elmap 
 |-  ( f e. ( C ^m B ) <-> f : B --> C )
23 19 22 bitr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( f : b --> ( Base ` e ) <-> f e. ( C ^m B ) ) )
24 15 sqxpeqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
25 24 ixpeq1d 
 |-  ( ( ( 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 ) ) )
26 16 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = ( Hom ` E ) )
27 26 4 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` e ) = J )
28 27 oveqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) = ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) )
29 simpll 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> d = D )
30 29 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = ( Hom ` D ) )
31 30 3 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Hom ` d ) = H )
32 31 fveq1d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Hom ` d ) ` z ) = ( H ` z ) )
33 28 32 oveq12d 
 |-  ( ( ( 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 ) ) )
34 33 ixpeq2dv 
 |-  ( ( ( 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 ) ) )
35 25 34 eqtrd 
 |-  ( ( ( 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 ) ) )
36 35 eleq2d 
 |-  ( ( ( 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 ) ) ) )
37 29 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = ( Id ` D ) )
38 37 5 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` d ) = .1. )
39 38 fveq1d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` d ) ` x ) = ( .1. ` x ) )
40 39 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( x g x ) ` ( .1. ` x ) ) )
41 16 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = ( Id ` E ) )
42 41 6 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( Id ` e ) = I )
43 42 fveq1d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( Id ` e ) ` ( f ` x ) ) = ( I ` ( f ` x ) ) )
44 40 43 eqeq12d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( Id ` e ) ` ( f ` x ) ) <-> ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) ) )
45 31 oveqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( x ( Hom ` d ) y ) = ( x H y ) )
46 31 oveqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( y ( Hom ` d ) z ) = ( y H z ) )
47 29 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( comp ` d ) = ( comp ` D ) )
48 47 7 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( comp ` d ) = .x. )
49 48 oveqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. x , y >. ( comp ` d ) z ) = ( <. x , y >. .x. z ) )
50 49 oveqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( n ( <. x , y >. ( comp ` d ) z ) m ) = ( n ( <. x , y >. .x. z ) m ) )
51 50 fveq2d 
 |-  ( ( ( 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 ) ) )
52 16 fveq2d 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( comp ` e ) = ( comp ` E ) )
53 52 8 eqtr4di 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( comp ` e ) = O )
54 53 oveqd 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( <. ( f ` x ) , ( f ` y ) >. ( comp ` e ) ( f ` z ) ) = ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) )
55 54 oveqd 
 |-  ( ( ( 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 ) ) )
56 51 55 eqeq12d 
 |-  ( ( ( 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 ) ) ) )
57 46 56 raleqbidv 
 |-  ( ( ( 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 ) ) ) )
58 45 57 raleqbidv 
 |-  ( ( ( 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 ) ) ) )
59 15 58 raleqbidv 
 |-  ( ( ( 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 ) ) ) )
60 15 59 raleqbidv 
 |-  ( ( ( 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 ) ) ) )
61 44 60 anbi12d 
 |-  ( ( ( 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 ) ) ) ) )
62 15 61 raleqbidv 
 |-  ( ( ( 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 ) ) ) ) )
63 23 36 62 3anbi123d 
 |-  ( ( ( 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 ) ) ) ) ) )
64 df-3an 
 |-  ( ( 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 ) ) ) ) )
65 63 64 bitrdi 
 |-  ( ( ( d = D /\ e = E ) /\ b = B ) -> ( ( f : b --> ( Base ` e ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` e ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` d ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` d ) ` x ) ) = ( ( Id ` e ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` d ) y ) A. n e. ( y ( Hom ` d ) z ) ( ( x g z ) ` ( n ( <. x , y >. ( comp ` d ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` e ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) <-> ( ( f e. ( C ^m B ) /\ g e. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) /\ A. x e. B ( ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x H y ) A. n e. ( y H z ) ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) ) )
66 11 14 65 sbcied2 
 |-  ( ( 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 ) ) ) ) ) )
67 66 opabbidv 
 |-  ( ( 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 ) ) ) ) } )
68 df-func 
 |-  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 ) ) ) ) } )
69 ovex 
 |-  ( C ^m B ) e. _V
70 snex 
 |-  { f } e. _V
71 ovex 
 |-  ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
72 71 rgenw 
 |-  A. z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
73 ixpexg 
 |-  ( 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 )
74 72 73 ax-mp 
 |-  X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) e. _V
75 70 74 xpex 
 |-  ( { f } X. X_ z e. ( B X. B ) ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) e. _V
76 69 75 iunex 
 |-  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
77 simpl 
 |-  ( ( ( 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 ) ) ) )
78 77 anim2i 
 |-  ( ( 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 ) ) ) ) )
79 78 2eximi 
 |-  ( 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 ) ) ) ) )
80 elopab 
 |-  ( 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 ) ) ) ) ) )
81 eliunxp 
 |-  ( 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 ) ) ) ) )
82 79 80 81 3imtr4i 
 |-  ( 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 ) ) ) )
83 82 ssriv 
 |-  { <. 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 ) ) )
84 76 83 ssexi 
 |-  { <. 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
85 67 68 84 ovmpoa 
 |-  ( ( 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 ) ) ) ) } )
86 9 10 85 syl2anc 
 |-  ( 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 ) ) ) ) } )
87 86 breqd 
 |-  ( 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 ) )
88 brabv 
 |-  ( 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 ) )
89 elex 
 |-  ( F e. ( C ^m B ) -> F e. _V )
90 elex 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) -> G e. _V )
91 89 90 anim12i 
 |-  ( ( 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 ) )
92 91 3adant3 
 |-  ( ( 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 ) )
93 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
94 93 eleq1d 
 |-  ( ( f = F /\ g = G ) -> ( f e. ( C ^m B ) <-> F e. ( C ^m B ) ) )
95 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
96 93 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` ( 1st ` z ) ) = ( F ` ( 1st ` z ) ) )
97 93 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` ( 2nd ` z ) ) = ( F ` ( 2nd ` z ) ) )
98 96 97 oveq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) = ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) )
99 98 oveq1d 
 |-  ( ( f = F /\ g = G ) -> ( ( ( f ` ( 1st ` z ) ) J ( f ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
100 99 ixpeq2dv 
 |-  ( ( 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 ) ) )
101 95 100 eleq12d 
 |-  ( ( 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 ) ) ) )
102 95 oveqd 
 |-  ( ( f = F /\ g = G ) -> ( x g x ) = ( x G x ) )
103 102 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( ( x g x ) ` ( .1. ` x ) ) = ( ( x G x ) ` ( .1. ` x ) ) )
104 93 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
105 104 fveq2d 
 |-  ( ( f = F /\ g = G ) -> ( I ` ( f ` x ) ) = ( I ` ( F ` x ) ) )
106 103 105 eqeq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( ( x g x ) ` ( .1. ` x ) ) = ( I ` ( f ` x ) ) <-> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) )
107 95 oveqd 
 |-  ( ( f = F /\ g = G ) -> ( x g z ) = ( x G z ) )
108 107 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( ( x g z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( x G z ) ` ( n ( <. x , y >. .x. z ) m ) ) )
109 93 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` y ) = ( F ` y ) )
110 104 109 opeq12d 
 |-  ( ( f = F /\ g = G ) -> <. ( f ` x ) , ( f ` y ) >. = <. ( F ` x ) , ( F ` y ) >. )
111 93 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` z ) = ( F ` z ) )
112 110 111 oveq12d 
 |-  ( ( f = F /\ g = G ) -> ( <. ( f ` x ) , ( f ` y ) >. O ( f ` z ) ) = ( <. ( F ` x ) , ( F ` y ) >. O ( F ` z ) ) )
113 95 oveqd 
 |-  ( ( f = F /\ g = G ) -> ( y g z ) = ( y G z ) )
114 113 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( ( y g z ) ` n ) = ( ( y G z ) ` n ) )
115 95 oveqd 
 |-  ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
116 115 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( ( x g y ) ` m ) = ( ( x G y ) ` m ) )
117 112 114 116 oveq123d 
 |-  ( ( 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 ) ) )
118 108 117 eqeq12d 
 |-  ( ( 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 ) ) ) )
119 118 2ralbidv 
 |-  ( ( 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 ) ) ) )
120 119 2ralbidv 
 |-  ( ( 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 ) ) ) )
121 106 120 anbi12d 
 |-  ( ( 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 ) ) ) ) )
122 121 ralbidv 
 |-  ( ( 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 ) ) ) ) )
123 94 101 122 3anbi123d 
 |-  ( ( 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 ) ) ) ) ) )
124 64 123 bitr3id 
 |-  ( ( 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 ) ) ) ) ) )
125 eqid 
 |-  { <. 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 ) ) ) ) }
126 124 125 brabga 
 |-  ( ( 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 ) ) ) ) ) )
127 88 92 126 pm5.21nii 
 |-  ( 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 ) ) ) ) )
128 20 21 elmap 
 |-  ( F e. ( C ^m B ) <-> F : B --> C )
129 128 3anbi1i 
 |-  ( ( 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 ) ) ) ) )
130 127 129 bitri 
 |-  ( 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 ) ) ) ) )
131 87 130 bitrdi 
 |-  ( 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 ) ) ) ) ) )