Metamath Proof Explorer

Theorem fucofvalg

Description: Value of the function giving the functor composition bifunctor. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses fucofvalg.p 
|- ( ph -> P e. U )
fucofvalg.c 
|- ( ph -> ( 1st ` P ) = C )
fucofvalg.d 
|- ( ph -> ( 2nd ` P ) = D )
fucofvalg.e 
|- ( ph -> E e. V )
fucofvalg.o 
|- ( ph -> ( P o.F E ) = .o. )
fucofvalg.w 
|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
Assertion fucofvalg 
|- ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 fucofvalg.p 
 |-  ( ph -> P e. U )
2 fucofvalg.c 
 |-  ( ph -> ( 1st ` P ) = C )
3 fucofvalg.d 
 |-  ( ph -> ( 2nd ` P ) = D )
4 fucofvalg.e 
 |-  ( ph -> E e. V )
5 fucofvalg.o 
 |-  ( ph -> ( P o.F E ) = .o. )
6 fucofvalg.w 
 |-  ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
7 df-fuco 
 |-  o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
8 7 a1i 
 |-  ( ph -> o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) )
9 fvexd 
 |-  ( ( ph /\ ( p = P /\ e = E ) ) -> ( 1st ` p ) e. _V )
10 simprl 
 |-  ( ( ph /\ ( p = P /\ e = E ) ) -> p = P )
11 10 fveq2d 
 |-  ( ( ph /\ ( p = P /\ e = E ) ) -> ( 1st ` p ) = ( 1st ` P ) )
12 2 adantr 
 |-  ( ( ph /\ ( p = P /\ e = E ) ) -> ( 1st ` P ) = C )
13 11 12 eqtrd 
 |-  ( ( ph /\ ( p = P /\ e = E ) ) -> ( 1st ` p ) = C )
14 fvexd 
 |-  ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) e. _V )
15 simplrl 
 |-  ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) -> p = P )
16 15 fveq2d 
 |-  ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) = ( 2nd ` P ) )
17 3 ad2antrr 
 |-  ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) -> ( 2nd ` P ) = D )
18 16 17 eqtrd 
 |-  ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) -> ( 2nd ` p ) = D )
19 simpr 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> d = D )
20 simpllr 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( p = P /\ e = E ) )
21 20 simprd 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> e = E )
22 19 21 oveq12d 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( d Func e ) = ( D Func E ) )
23 simplr 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> c = C )
24 23 19 oveq12d 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( c Func d ) = ( C Func D ) )
25 22 24 xpeq12d 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( d Func e ) X. ( c Func d ) ) = ( ( D Func E ) X. ( C Func D ) ) )
26 ovexd 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( D Func E ) e. _V )
27 ovexd 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( C Func D ) e. _V )
28 26 27 xpexd 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( D Func E ) X. ( C Func D ) ) e. _V )
29 25 28 eqeltrd 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( d Func e ) X. ( c Func d ) ) e. _V )
30 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> W = ( ( D Func E ) X. ( C Func D ) ) )
31 25 30 eqtr4d 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( d Func e ) X. ( c Func d ) ) = W )
32 simpr 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> w = W )
33 32 reseq2d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( o.func |` w ) = ( o.func |` W ) )
34 simplr 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> d = D )
35 21 adantr 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> e = E )
36 34 35 oveq12d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( d Nat e ) = ( D Nat E ) )
37 36 oveqd 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) = ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) )
38 simpllr 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> c = C )
39 38 34 oveq12d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( c Nat d ) = ( C Nat D ) )
40 39 oveqd 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) = ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) )
41 38 fveq2d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( Base ` c ) = ( Base ` C ) )
42 35 fveq2d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( comp ` e ) = ( comp ` E ) )
43 42 oveqd 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) = ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) )
44 43 oveqd 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) = ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) )
45 41 44 mpteq12dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) = ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
46 37 40 45 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) = ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
47 46 csbeq2dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) = [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
48 47 csbeq2dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) = [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
49 48 csbeq2dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) = [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
50 49 csbeq2dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) = [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
51 50 csbeq2dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) = [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
52 32 32 51 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) = ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) )
53 33 52 opeq12d 
 |-  ( ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) /\ w = W ) -> <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
54 29 31 53 csbied2 
 |-  ( ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) /\ d = D ) -> [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
55 14 18 54 csbied2 
 |-  ( ( ( ph /\ ( p = P /\ e = E ) ) /\ c = C ) -> [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
56 9 13 55 csbied2 
 |-  ( ( ph /\ ( p = P /\ e = E ) ) -> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
57 1 elexd 
 |-  ( ph -> P e. _V )
58 4 elexd 
 |-  ( ph -> E e. _V )
59 opex 
 |-  <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. e. _V
60 59 a1i 
 |-  ( ph -> <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. e. _V )
61 8 56 57 58 60 ovmpod 
 |-  ( ph -> ( P o.F E ) = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
62 5 61 eqtr3d 
 |-  ( ph -> .o. = <. ( o.func |` W ) , ( u e. W , v e. W |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) |-> ( x e. ( Base ` C ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )