Metamath Proof Explorer

Theorem fuco21

Description: The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses fuco11.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco11.f 
|- ( ph -> F ( C Func D ) G )
fuco11.k 
|- ( ph -> K ( D Func E ) L )
fuco11.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
fuco21.m 
|- ( ph -> M ( C Func D ) N )
fuco21.r 
|- ( ph -> R ( D Func E ) S )
fuco21.v 
|- ( ph -> V = <. <. R , S >. , <. M , N >. >. )
Assertion fuco21 
|- ( ph -> ( U P V ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 fuco11.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco11.f 
 |-  ( ph -> F ( C Func D ) G )
3 fuco11.k 
 |-  ( ph -> K ( D Func E ) L )
4 fuco11.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
5 fuco21.m 
 |-  ( ph -> M ( C Func D ) N )
6 fuco21.r 
 |-  ( ph -> R ( D Func E ) S )
7 fuco21.v 
 |-  ( ph -> V = <. <. R , S >. , <. M , N >. >. )
8 2 funcrcl2 
 |-  ( ph -> C e. Cat )
9 3 funcrcl2 
 |-  ( ph -> D e. Cat )
10 3 funcrcl3 
 |-  ( ph -> E e. Cat )
11 eqidd 
 |-  ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
12 8 9 10 1 11 fuco2 
 |-  ( ph -> P = ( u e. ( ( D Func E ) X. ( C Func D ) ) , v e. ( ( D Func E ) X. ( C Func D ) ) |-> [_ ( 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 ) ) ) ) ) ) )
13 fvexd 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> ( 1st ` ( 2nd ` u ) ) e. _V )
14 simprl 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> u = U )
15 4 adantr 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> U = <. <. K , L >. , <. F , G >. >. )
16 14 15 eqtrd 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> u = <. <. K , L >. , <. F , G >. >. )
17 16 fveq2d 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> ( 2nd ` u ) = ( 2nd ` <. <. K , L >. , <. F , G >. >. ) )
18 17 fveq2d 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> ( 1st ` ( 2nd ` u ) ) = ( 1st ` ( 2nd ` <. <. K , L >. , <. F , G >. >. ) ) )
19 opex 
 |-  <. K , L >. e. _V
20 opex 
 |-  <. F , G >. e. _V
21 19 20 op2nd 
 |-  ( 2nd ` <. <. K , L >. , <. F , G >. >. ) = <. F , G >.
22 21 fveq2i 
 |-  ( 1st ` ( 2nd ` <. <. K , L >. , <. F , G >. >. ) ) = ( 1st ` <. F , G >. )
23 relfunc 
 |-  Rel ( C Func D )
24 23 brrelex1i 
 |-  ( F ( C Func D ) G -> F e. _V )
25 2 24 syl 
 |-  ( ph -> F e. _V )
26 23 brrelex2i 
 |-  ( F ( C Func D ) G -> G e. _V )
27 2 26 syl 
 |-  ( ph -> G e. _V )
28 op1stg 
 |-  ( ( F e. _V /\ G e. _V ) -> ( 1st ` <. F , G >. ) = F )
29 25 27 28 syl2anc 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
30 22 29 eqtrid 
 |-  ( ph -> ( 1st ` ( 2nd ` <. <. K , L >. , <. F , G >. >. ) ) = F )
31 30 adantr 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> ( 1st ` ( 2nd ` <. <. K , L >. , <. F , G >. >. ) ) = F )
32 18 31 eqtrd 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> ( 1st ` ( 2nd ` u ) ) = F )
33 fvexd 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> ( 1st ` ( 1st ` u ) ) e. _V )
34 14 adantr 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> u = U )
35 15 adantr 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> U = <. <. K , L >. , <. F , G >. >. )
36 34 35 eqtrd 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> u = <. <. K , L >. , <. F , G >. >. )
37 36 fveq2d 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> ( 1st ` u ) = ( 1st ` <. <. K , L >. , <. F , G >. >. ) )
38 37 fveq2d 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> ( 1st ` ( 1st ` u ) ) = ( 1st ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) )
39 19 20 op1st 
 |-  ( 1st ` <. <. K , L >. , <. F , G >. >. ) = <. K , L >.
40 39 fveq2i 
 |-  ( 1st ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) = ( 1st ` <. K , L >. )
41 relfunc 
 |-  Rel ( D Func E )
42 41 brrelex1i 
 |-  ( K ( D Func E ) L -> K e. _V )
43 3 42 syl 
 |-  ( ph -> K e. _V )
44 41 brrelex2i 
 |-  ( K ( D Func E ) L -> L e. _V )
45 3 44 syl 
 |-  ( ph -> L e. _V )
46 op1stg 
 |-  ( ( K e. _V /\ L e. _V ) -> ( 1st ` <. K , L >. ) = K )
47 43 45 46 syl2anc 
 |-  ( ph -> ( 1st ` <. K , L >. ) = K )
48 40 47 eqtrid 
 |-  ( ph -> ( 1st ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) = K )
49 48 ad2antrr 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> ( 1st ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) = K )
50 38 49 eqtrd 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) -> ( 1st ` ( 1st ` u ) ) = K )
51 fvexd 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> ( 2nd ` ( 1st ` u ) ) e. _V )
52 34 adantr 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> u = U )
53 35 adantr 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> U = <. <. K , L >. , <. F , G >. >. )
54 52 53 eqtrd 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> u = <. <. K , L >. , <. F , G >. >. )
55 54 fveq2d 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> ( 1st ` u ) = ( 1st ` <. <. K , L >. , <. F , G >. >. ) )
56 55 fveq2d 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> ( 2nd ` ( 1st ` u ) ) = ( 2nd ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) )
57 39 fveq2i 
 |-  ( 2nd ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) = ( 2nd ` <. K , L >. )
58 op2ndg 
 |-  ( ( K e. _V /\ L e. _V ) -> ( 2nd ` <. K , L >. ) = L )
59 43 45 58 syl2anc 
 |-  ( ph -> ( 2nd ` <. K , L >. ) = L )
60 57 59 eqtrid 
 |-  ( ph -> ( 2nd ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) = L )
61 60 ad3antrrr 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> ( 2nd ` ( 1st ` <. <. K , L >. , <. F , G >. >. ) ) = L )
62 56 61 eqtrd 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) -> ( 2nd ` ( 1st ` u ) ) = L )
63 fvexd 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> ( 1st ` ( 2nd ` v ) ) e. _V )
64 simp-4r 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> ( u = U /\ v = V ) )
65 64 simprd 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> v = V )
66 7 ad4antr 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> V = <. <. R , S >. , <. M , N >. >. )
67 65 66 eqtrd 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> v = <. <. R , S >. , <. M , N >. >. )
68 67 fveq2d 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> ( 2nd ` v ) = ( 2nd ` <. <. R , S >. , <. M , N >. >. ) )
69 68 fveq2d 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> ( 1st ` ( 2nd ` v ) ) = ( 1st ` ( 2nd ` <. <. R , S >. , <. M , N >. >. ) ) )
70 opex 
 |-  <. R , S >. e. _V
71 opex 
 |-  <. M , N >. e. _V
72 70 71 op2nd 
 |-  ( 2nd ` <. <. R , S >. , <. M , N >. >. ) = <. M , N >.
73 72 fveq2i 
 |-  ( 1st ` ( 2nd ` <. <. R , S >. , <. M , N >. >. ) ) = ( 1st ` <. M , N >. )
74 23 brrelex1i 
 |-  ( M ( C Func D ) N -> M e. _V )
75 5 74 syl 
 |-  ( ph -> M e. _V )
76 23 brrelex2i 
 |-  ( M ( C Func D ) N -> N e. _V )
77 5 76 syl 
 |-  ( ph -> N e. _V )
78 op1stg 
 |-  ( ( M e. _V /\ N e. _V ) -> ( 1st ` <. M , N >. ) = M )
79 75 77 78 syl2anc 
 |-  ( ph -> ( 1st ` <. M , N >. ) = M )
80 73 79 eqtrid 
 |-  ( ph -> ( 1st ` ( 2nd ` <. <. R , S >. , <. M , N >. >. ) ) = M )
81 80 ad4antr 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> ( 1st ` ( 2nd ` <. <. R , S >. , <. M , N >. >. ) ) = M )
82 69 81 eqtrd 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) -> ( 1st ` ( 2nd ` v ) ) = M )
83 fvexd 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> ( 1st ` ( 1st ` v ) ) e. _V )
84 65 adantr 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> v = V )
85 66 adantr 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> V = <. <. R , S >. , <. M , N >. >. )
86 84 85 eqtrd 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> v = <. <. R , S >. , <. M , N >. >. )
87 86 fveq2d 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> ( 1st ` v ) = ( 1st ` <. <. R , S >. , <. M , N >. >. ) )
88 87 fveq2d 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> ( 1st ` ( 1st ` v ) ) = ( 1st ` ( 1st ` <. <. R , S >. , <. M , N >. >. ) ) )
89 70 71 op1st 
 |-  ( 1st ` <. <. R , S >. , <. M , N >. >. ) = <. R , S >.
90 89 fveq2i 
 |-  ( 1st ` ( 1st ` <. <. R , S >. , <. M , N >. >. ) ) = ( 1st ` <. R , S >. )
91 41 brrelex1i 
 |-  ( R ( D Func E ) S -> R e. _V )
92 6 91 syl 
 |-  ( ph -> R e. _V )
93 41 brrelex2i 
 |-  ( R ( D Func E ) S -> S e. _V )
94 6 93 syl 
 |-  ( ph -> S e. _V )
95 op1stg 
 |-  ( ( R e. _V /\ S e. _V ) -> ( 1st ` <. R , S >. ) = R )
96 92 94 95 syl2anc 
 |-  ( ph -> ( 1st ` <. R , S >. ) = R )
97 90 96 eqtrid 
 |-  ( ph -> ( 1st ` ( 1st ` <. <. R , S >. , <. M , N >. >. ) ) = R )
98 97 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> ( 1st ` ( 1st ` <. <. R , S >. , <. M , N >. >. ) ) = R )
99 88 98 eqtrd 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) -> ( 1st ` ( 1st ` v ) ) = R )
100 55 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 1st ` u ) = ( 1st ` <. <. K , L >. , <. F , G >. >. ) )
101 100 39 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 1st ` u ) = <. K , L >. )
102 87 adantr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 1st ` v ) = ( 1st ` <. <. R , S >. , <. M , N >. >. ) )
103 102 89 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 1st ` v ) = <. R , S >. )
104 101 103 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( ( 1st ` u ) ( D Nat E ) ( 1st ` v ) ) = ( <. K , L >. ( D Nat E ) <. R , S >. ) )
105 17 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 2nd ` u ) = ( 2nd ` <. <. K , L >. , <. F , G >. >. ) )
106 105 21 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 2nd ` u ) = <. F , G >. )
107 68 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 2nd ` v ) = ( 2nd ` <. <. R , S >. , <. M , N >. >. ) )
108 107 72 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 2nd ` v ) = <. M , N >. )
109 106 108 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( ( 2nd ` u ) ( C Nat D ) ( 2nd ` v ) ) = ( <. F , G >. ( C Nat D ) <. M , N >. ) )
110 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> k = K )
111 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> f = F )
112 111 fveq1d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( f ` x ) = ( F ` x ) )
113 110 112 fveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( k ` ( f ` x ) ) = ( K ` ( F ` x ) ) )
114 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> m = M )
115 114 fveq1d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( m ` x ) = ( M ` x ) )
116 110 115 fveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( k ` ( m ` x ) ) = ( K ` ( M ` x ) ) )
117 113 116 opeq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. = <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. )
118 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> r = R )
119 118 115 fveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( r ` ( m ` x ) ) = ( R ` ( M ` x ) ) )
120 117 119 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` E ) ( r ` ( m ` x ) ) ) = ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) )
121 115 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( b ` ( m ` x ) ) = ( b ` ( M ` x ) ) )
122 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> l = L )
123 122 112 115 oveq123d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( ( f ` x ) l ( m ` x ) ) = ( ( F ` x ) L ( M ` x ) ) )
124 123 fveq1d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) = ( ( ( F ` x ) L ( M ` x ) ) ` ( a ` x ) ) )
125 120 121 124 oveq123d 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( ( 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 ) ) ) )
126 125 mpteq2dv 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = R ) -> ( 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 ) ) ) ) )
127 104 109 126 mpoeq123dv 
 |-  ( ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = M ) /\ r = 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 ) ) ) ) ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
128 83 99 127 csbied2 
 |-  ( ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = L ) /\ m = 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 ) ) ) ) ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
129 63 82 128 csbied2 
 |-  ( ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = K ) /\ l = 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 ) ) ) ) ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
130 51 62 129 csbied2 
 |-  ( ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = F ) /\ k = 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 ) ) ) ) ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
131 33 50 130 csbied2 
 |-  ( ( ( ph /\ ( u = U /\ v = V ) ) /\ f = 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 ) ) ) ) ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
132 13 32 131 csbied2 
 |-  ( ( ph /\ ( u = U /\ v = V ) ) -> [_ ( 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 ) ) ) ) ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )
133 11 4 3 2 fuco2eld 
 |-  ( ph -> U e. ( ( D Func E ) X. ( C Func D ) ) )
134 11 7 6 5 fuco2eld 
 |-  ( ph -> V e. ( ( D Func E ) X. ( C Func D ) ) )
135 ovex 
 |-  ( <. K , L >. ( D Nat E ) <. R , S >. ) e. _V
136 ovex 
 |-  ( <. F , G >. ( C Nat D ) <. M , N >. ) e. _V
137 135 136 mpoex 
 |-  ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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
138 137 a1i 
 |-  ( ph -> ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 )
139 12 132 133 134 138 ovmpod 
 |-  ( ph -> ( U P V ) = ( b e. ( <. K , L >. ( D Nat E ) <. R , S >. ) , a e. ( <. F , G >. ( C Nat D ) <. M , N >. ) |-> ( 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 ) ) ) ) ) )