Metamath Proof Explorer

Theorem fuco22natlem

Description: The composed natural transformation is a natural transformation. Use fuco22nat instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fuco22natlem.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco22natlem.a 
|- ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
fuco22natlem.b 
|- ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
fuco22natlem.u 
|- ( ph -> U = <. <. K , L >. , <. F , G >. >. )
fuco22natlem.v 
|- ( ph -> V = <. <. R , S >. , <. M , N >. >. )
Assertion fuco22natlem 
|- ( ph -> ( B ( U P V ) A ) e. ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )

Proof

Step Hyp Ref Expression
1 fuco22natlem.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco22natlem.a 
 |-  ( ph -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
3 fuco22natlem.b 
 |-  ( ph -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
4 fuco22natlem.u 
 |-  ( ph -> U = <. <. K , L >. , <. F , G >. >. )
5 fuco22natlem.v 
 |-  ( ph -> V = <. <. R , S >. , <. M , N >. >. )
6 eqid 
 |-  ( C Nat E ) = ( C Nat E )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
10 eqid 
 |-  ( comp ` E ) = ( comp ` E )
11 eqid 
 |-  ( C Nat D ) = ( C Nat D )
12 11 2 natrcl2 
 |-  ( ph -> F ( C Func D ) G )
13 eqid 
 |-  ( D Nat E ) = ( D Nat E )
14 13 3 natrcl2 
 |-  ( ph -> K ( D Func E ) L )
15 1 12 14 4 7 fuco11a 
 |-  ( ph -> ( O ` U ) = <. ( K o. F ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) >. )
16 1 12 14 4 fuco11cl 
 |-  ( ph -> ( O ` U ) e. ( C Func E ) )
17 15 16 eqeltrrd 
 |-  ( ph -> <. ( K o. F ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) >. e. ( C Func E ) )
18 df-br 
 |-  ( ( K o. F ) ( C Func E ) ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) <-> <. ( K o. F ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) >. e. ( C Func E ) )
19 17 18 sylibr 
 |-  ( ph -> ( K o. F ) ( C Func E ) ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) )
20 11 2 natrcl3 
 |-  ( ph -> M ( C Func D ) N )
21 13 3 natrcl3 
 |-  ( ph -> R ( D Func E ) S )
22 1 20 21 5 7 fuco11a 
 |-  ( ph -> ( O ` V ) = <. ( R o. M ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) >. )
23 1 20 21 5 fuco11cl 
 |-  ( ph -> ( O ` V ) e. ( C Func E ) )
24 22 23 eqeltrrd 
 |-  ( ph -> <. ( R o. M ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) >. e. ( C Func E ) )
25 df-br 
 |-  ( ( R o. M ) ( C Func E ) ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) <-> <. ( R o. M ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) >. e. ( C Func E ) )
26 24 25 sylibr 
 |-  ( ph -> ( R o. M ) ( C Func E ) ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) )
27 1 4 5 2 3 fucofn22 
 |-  ( ph -> ( B ( U P V ) A ) Fn ( Base ` C ) )
28 eqid 
 |-  ( Base ` E ) = ( Base ` E )
29 14 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> K ( D Func E ) L )
30 29 funcrcl3 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E e. Cat )
31 eqid 
 |-  ( Base ` D ) = ( Base ` D )
32 31 28 29 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> K : ( Base ` D ) --> ( Base ` E ) )
33 12 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F ( C Func D ) G )
34 7 31 33 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F : ( Base ` C ) --> ( Base ` D ) )
35 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
36 34 35 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( F ` x ) e. ( Base ` D ) )
37 32 36 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( K ` ( F ` x ) ) e. ( Base ` E ) )
38 20 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> M ( C Func D ) N )
39 7 31 38 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> M : ( Base ` C ) --> ( Base ` D ) )
40 39 35 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( M ` x ) e. ( Base ` D ) )
41 32 40 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( K ` ( M ` x ) ) e. ( Base ` E ) )
42 21 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R ( D Func E ) S )
43 31 28 42 funcf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> R : ( Base ` D ) --> ( Base ` E ) )
44 43 40 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( R ` ( M ` x ) ) e. ( Base ` E ) )
45 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
46 31 45 9 29 36 40 funcf2 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( F ` x ) L ( M ` x ) ) : ( ( F ` x ) ( Hom ` D ) ( M ` x ) ) --> ( ( K ` ( F ` x ) ) ( Hom ` E ) ( K ` ( M ` x ) ) ) )
47 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
48 11 47 7 45 35 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( A ` x ) e. ( ( F ` x ) ( Hom ` D ) ( M ` x ) ) )
49 46 48 ffvelcdmd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) e. ( ( K ` ( F ` x ) ) ( Hom ` E ) ( K ` ( M ` x ) ) ) )
50 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
51 7 31 20 funcf1 
 |-  ( ph -> M : ( Base ` C ) --> ( Base ` D ) )
52 51 ffvelcdmda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( M ` x ) e. ( Base ` D ) )
53 13 50 31 9 52 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( B ` ( M ` x ) ) e. ( ( K ` ( M ` x ) ) ( Hom ` E ) ( R ` ( M ` x ) ) ) )
54 28 9 10 30 37 41 44 49 53 catcocl 
 |-  ( ( ph /\ 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. ( ( K ` ( F ` x ) ) ( Hom ` E ) ( R ` ( M ` x ) ) ) )
55 1 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
56 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> U = <. <. K , L >. , <. F , G >. >. )
57 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> V = <. <. R , S >. , <. M , N >. >. )
58 eqidd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) = ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) )
59 55 56 57 47 50 35 58 fuco23 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( B ( U P V ) A ) ` x ) = ( ( B ` ( M ` x ) ) ( <. ( K ` ( F ` x ) ) , ( K ` ( M ` x ) ) >. ( comp ` E ) ( R ` ( M ` x ) ) ) ( ( ( F ` x ) L ( M ` x ) ) ` ( A ` x ) ) ) )
60 34 35 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( K o. F ) ` x ) = ( K ` ( F ` x ) ) )
61 39 35 fvco3d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( R o. M ) ` x ) = ( R ` ( M ` x ) ) )
62 60 61 oveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( ( K o. F ) ` x ) ( Hom ` E ) ( ( R o. M ) ` x ) ) = ( ( K ` ( F ` x ) ) ( Hom ` E ) ( R ` ( M ` x ) ) ) )
63 54 59 62 3eltr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( B ( U P V ) A ) ` x ) e. ( ( ( K o. F ) ` x ) ( Hom ` E ) ( ( R o. M ) ` x ) ) )
64 simplrl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
65 simplrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
66 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> A e. ( <. F , G >. ( C Nat D ) <. M , N >. ) )
67 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> h e. ( x ( Hom ` C ) y ) )
68 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> B e. ( <. K , L >. ( D Nat E ) <. R , S >. ) )
69 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
70 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> U = <. <. K , L >. , <. F , G >. >. )
71 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> V = <. <. R , S >. , <. M , N >. >. )
72 64 65 66 67 68 69 70 71 fuco22natlem3 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( ( B ( U P V ) A ) ` y ) ( <. ( ( K o. F ) ` x ) , ( ( K o. F ) ` y ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ` h ) ) = ( ( ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) ` h ) ( <. ( ( K o. F ) ` x ) , ( ( R o. M ) ` x ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( B ( U P V ) A ) ` x ) ) )
73 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
74 73 oveq1d 
 |-  ( z = x -> ( ( F ` z ) L ( F ` w ) ) = ( ( F ` x ) L ( F ` w ) ) )
75 oveq1 
 |-  ( z = x -> ( z G w ) = ( x G w ) )
76 74 75 coeq12d 
 |-  ( z = x -> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) = ( ( ( F ` x ) L ( F ` w ) ) o. ( x G w ) ) )
77 fveq2 
 |-  ( w = y -> ( F ` w ) = ( F ` y ) )
78 77 oveq2d 
 |-  ( w = y -> ( ( F ` x ) L ( F ` w ) ) = ( ( F ` x ) L ( F ` y ) ) )
79 oveq2 
 |-  ( w = y -> ( x G w ) = ( x G y ) )
80 78 79 coeq12d 
 |-  ( w = y -> ( ( ( F ` x ) L ( F ` w ) ) o. ( x G w ) ) = ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) )
81 eqid 
 |-  ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) = ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) )
82 ovex 
 |-  ( ( F ` x ) L ( F ` y ) ) e. _V
83 ovex 
 |-  ( x G y ) e. _V
84 82 83 coex 
 |-  ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) e. _V
85 76 80 81 84 ovmpo 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) y ) = ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) )
86 85 ad2antlr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) y ) = ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) )
87 86 fveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) y ) ` h ) = ( ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ` h ) )
88 87 oveq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( ( B ( U P V ) A ) ` y ) ( <. ( ( K o. F ) ` x ) , ( ( K o. F ) ` y ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) y ) ` h ) ) = ( ( ( B ( U P V ) A ) ` y ) ( <. ( ( K o. F ) ` x ) , ( ( K o. F ) ` y ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( ( ( F ` x ) L ( F ` y ) ) o. ( x G y ) ) ` h ) ) )
89 fveq2 
 |-  ( z = x -> ( M ` z ) = ( M ` x ) )
90 89 oveq1d 
 |-  ( z = x -> ( ( M ` z ) S ( M ` w ) ) = ( ( M ` x ) S ( M ` w ) ) )
91 oveq1 
 |-  ( z = x -> ( z N w ) = ( x N w ) )
92 90 91 coeq12d 
 |-  ( z = x -> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) = ( ( ( M ` x ) S ( M ` w ) ) o. ( x N w ) ) )
93 fveq2 
 |-  ( w = y -> ( M ` w ) = ( M ` y ) )
94 93 oveq2d 
 |-  ( w = y -> ( ( M ` x ) S ( M ` w ) ) = ( ( M ` x ) S ( M ` y ) ) )
95 oveq2 
 |-  ( w = y -> ( x N w ) = ( x N y ) )
96 94 95 coeq12d 
 |-  ( w = y -> ( ( ( M ` x ) S ( M ` w ) ) o. ( x N w ) ) = ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) )
97 eqid 
 |-  ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) = ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) )
98 ovex 
 |-  ( ( M ` x ) S ( M ` y ) ) e. _V
99 ovex 
 |-  ( x N y ) e. _V
100 98 99 coex 
 |-  ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) e. _V
101 92 96 97 100 ovmpo 
 |-  ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) y ) = ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) )
102 101 ad2antlr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) y ) = ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) )
103 102 fveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) y ) ` h ) = ( ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) ` h ) )
104 103 oveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) y ) ` h ) ( <. ( ( K o. F ) ` x ) , ( ( R o. M ) ` x ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( B ( U P V ) A ) ` x ) ) = ( ( ( ( ( M ` x ) S ( M ` y ) ) o. ( x N y ) ) ` h ) ( <. ( ( K o. F ) ` x ) , ( ( R o. M ) ` x ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( B ( U P V ) A ) ` x ) ) )
105 72 88 104 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( ( ( B ( U P V ) A ) ` y ) ( <. ( ( K o. F ) ` x ) , ( ( K o. F ) ` y ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) y ) ` h ) ) = ( ( ( x ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) y ) ` h ) ( <. ( ( K o. F ) ` x ) , ( ( R o. M ) ` x ) >. ( comp ` E ) ( ( R o. M ) ` y ) ) ( ( B ( U P V ) A ) ` x ) ) )
106 6 7 8 9 10 19 26 27 63 105 isnatd 
 |-  ( ph -> ( B ( U P V ) A ) e. ( <. ( K o. F ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) >. ( C Nat E ) <. ( R o. M ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) >. ) )
107 15 22 oveq12d 
 |-  ( ph -> ( ( O ` U ) ( C Nat E ) ( O ` V ) ) = ( <. ( K o. F ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( F ` z ) L ( F ` w ) ) o. ( z G w ) ) ) >. ( C Nat E ) <. ( R o. M ) , ( z e. ( Base ` C ) , w e. ( Base ` C ) |-> ( ( ( M ` z ) S ( M ` w ) ) o. ( z N w ) ) ) >. ) )
108 106 107 eleqtrrd 
 |-  ( ph -> ( B ( U P V ) A ) e. ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )