Metamath Proof Explorer

Theorem precofvalALT

Description: Alternate proof of precofval . (Contributed by Zhi Wang, 11-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses precofval.q 
|- Q = ( C FuncCat D )
precofval.r 
|- R = ( D FuncCat E )
precofval.o 
|- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
precofval.f 
|- ( ph -> F e. ( C Func D ) )
precofval.e 
|- ( ph -> E e. Cat )
precofval.k 
|- ( ph -> K = ( ( 1st ` .o. ) ` F ) )
Assertion precofvalALT 
|- ( ph -> K = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. )

Proof

Step Hyp Ref Expression
1 precofval.q 
 |-  Q = ( C FuncCat D )
2 precofval.r 
 |-  R = ( D FuncCat E )
3 precofval.o 
 |-  ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) )
4 precofval.f 
 |-  ( ph -> F e. ( C Func D ) )
5 precofval.e 
 |-  ( ph -> E e. Cat )
6 precofval.k 
 |-  ( ph -> K = ( ( 1st ` .o. ) ` F ) )
7 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
8 relfunc 
 |-  Rel ( C Func D )
9 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
10 8 4 9 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
11 10 funcrcl2 
 |-  ( ph -> C e. Cat )
12 10 funcrcl3 
 |-  ( ph -> D e. Cat )
13 1 11 12 fuccat 
 |-  ( ph -> Q e. Cat )
14 2 12 5 fuccat 
 |-  ( ph -> R e. Cat )
15 2 1 oveq12i 
 |-  ( R Xc. Q ) = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
16 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
17 15 16 11 12 5 fucofunca 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( ( R Xc. Q ) Func ( C FuncCat E ) ) )
18 2 fucbas 
 |-  ( D Func E ) = ( Base ` R )
19 eqid 
 |-  ( D Nat E ) = ( D Nat E )
20 2 19 fuchom 
 |-  ( D Nat E ) = ( Hom ` R )
21 eqid 
 |-  ( Id ` Q ) = ( Id ` Q )
22 3 7 13 14 17 4 6 18 20 21 tposcurf1 
 |-  ( ph -> K = <. ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) >. )
23 df-ov 
 |-  ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) = ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. )
24 eqidd 
 |-  ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) )
25 11 12 5 24 fucoelvv 
 |-  ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) )
26 1st2nd2 
 |-  ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
27 25 26 syl 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
28 27 adantr 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
29 10 adantr 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
30 relfunc 
 |-  Rel ( D Func E )
31 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ g e. ( D Func E ) ) -> ( 1st ` g ) ( D Func E ) ( 2nd ` g ) )
32 30 31 mpan 
 |-  ( g e. ( D Func E ) -> ( 1st ` g ) ( D Func E ) ( 2nd ` g ) )
33 32 adantl 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( 1st ` g ) ( D Func E ) ( 2nd ` g ) )
34 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ g e. ( D Func E ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
35 30 34 mpan 
 |-  ( g e. ( D Func E ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
36 35 adantl 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> g = <. ( 1st ` g ) , ( 2nd ` g ) >. )
37 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
38 8 4 37 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
39 38 adantr 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
40 36 39 opeq12d 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> <. g , F >. = <. <. ( 1st ` g ) , ( 2nd ` g ) >. , <. ( 1st ` F ) , ( 2nd ` F ) >. >. )
41 28 29 33 40 fuco11 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) = ( <. ( 1st ` g ) , ( 2nd ` g ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
42 36 39 oveq12d 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( g o.func F ) = ( <. ( 1st ` g ) , ( 2nd ` g ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
43 41 42 eqtr4d 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. g , F >. ) = ( g o.func F ) )
44 23 43 eqtrid 
 |-  ( ( ph /\ g e. ( D Func E ) ) -> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) = ( g o.func F ) )
45 44 mpteq2dva 
 |-  ( ph -> ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) = ( g e. ( D Func E ) |-> ( g o.func F ) ) )
46 eqid 
 |-  ( Id ` D ) = ( Id ` D )
47 1 21 46 4 fucid 
 |-  ( ph -> ( ( Id ` Q ) ` F ) = ( ( Id ` D ) o. ( 1st ` F ) ) )
48 47 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( ( Id ` Q ) ` F ) = ( ( Id ` D ) o. ( 1st ` F ) ) )
49 48 oveq2d 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) = ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` D ) o. ( 1st ` F ) ) ) )
50 27 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. )
51 eqidd 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> <. g , F >. = <. g , F >. )
52 eqidd 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> <. h , F >. = <. h , F >. )
53 eqid 
 |-  ( C Nat D ) = ( C Nat D )
54 1 53 46 4 fucidcl 
 |-  ( ph -> ( ( Id ` D ) o. ( 1st ` F ) ) e. ( F ( C Nat D ) F ) )
55 54 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( ( Id ` D ) o. ( 1st ` F ) ) e. ( F ( C Nat D ) F ) )
56 simpr 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> a e. ( g ( D Nat E ) h ) )
57 50 51 52 55 56 fuco22a 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` D ) o. ( 1st ` F ) ) ) = ( x e. ( Base ` C ) |-> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) ) ) )
58 eqid 
 |-  ( Base ` C ) = ( Base ` C )
59 eqid 
 |-  ( Base ` E ) = ( Base ` E )
60 eqid 
 |-  ( Id ` E ) = ( Id ` E )
61 10 ad3antrrr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
62 32 adantr 
 |-  ( ( g e. ( D Func E ) /\ h e. ( D Func E ) ) -> ( 1st ` g ) ( D Func E ) ( 2nd ` g ) )
63 62 ad3antlr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( 1st ` g ) ( D Func E ) ( 2nd ` g ) )
64 simpr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
65 58 59 46 60 61 63 64 precofvallem 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) ) /\ ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) e. ( Base ` E ) ) )
66 65 simpld 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) = ( ( Id ` E ) ` ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) ) )
67 66 oveq2d 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) ) = ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( Id ` E ) ` ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) ) ) )
68 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
69 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> E e. Cat )
70 65 simprd 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) e. ( Base ` E ) )
71 eqid 
 |-  ( comp ` E ) = ( comp ` E )
72 eqid 
 |-  ( Base ` D ) = ( Base ` D )
73 simpllr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( g e. ( D Func E ) /\ h e. ( D Func E ) ) )
74 73 simprd 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> h e. ( D Func E ) )
75 1st2ndbr 
 |-  ( ( Rel ( D Func E ) /\ h e. ( D Func E ) ) -> ( 1st ` h ) ( D Func E ) ( 2nd ` h ) )
76 30 74 75 sylancr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( 1st ` h ) ( D Func E ) ( 2nd ` h ) )
77 72 59 76 funcf1 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( 1st ` h ) : ( Base ` D ) --> ( Base ` E ) )
78 10 ad2antrr 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
79 58 72 78 funcf1 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
80 79 ffvelcdmda 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
81 77 80 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) e. ( Base ` E ) )
82 56 adantr 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> a e. ( g ( D Nat E ) h ) )
83 19 82 nat1st2nd 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> a e. ( <. ( 1st ` g ) , ( 2nd ` g ) >. ( D Nat E ) <. ( 1st ` h ) , ( 2nd ` h ) >. ) )
84 19 83 72 68 80 natcl 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( a ` ( ( 1st ` F ) ` x ) ) e. ( ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) ( Hom ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) )
85 59 68 60 69 70 71 81 84 catrid 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( Id ` E ) ` ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) ) ) = ( a ` ( ( 1st ` F ) ` x ) ) )
86 67 85 eqtrd 
 |-  ( ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) /\ x e. ( Base ` C ) ) -> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) ) = ( a ` ( ( 1st ` F ) ` x ) ) )
87 86 mpteq2dva 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( x e. ( Base ` C ) |-> ( ( a ` ( ( 1st ` F ) ` x ) ) ( <. ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) , ( ( 1st ` g ) ` ( ( 1st ` F ) ` x ) ) >. ( comp ` E ) ( ( 1st ` h ) ` ( ( 1st ` F ) ` x ) ) ) ( ( ( ( 1st ` F ) ` x ) ( 2nd ` g ) ( ( 1st ` F ) ` x ) ) ` ( ( ( Id ` D ) o. ( 1st ` F ) ) ` x ) ) ) ) = ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) )
88 49 57 87 3eqtrd 
 |-  ( ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) /\ a e. ( g ( D Nat E ) h ) ) -> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) = ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) )
89 88 mpteq2dva 
 |-  ( ( ph /\ ( g e. ( D Func E ) /\ h e. ( D Func E ) ) ) -> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) )
90 89 3impb 
 |-  ( ( ph /\ g e. ( D Func E ) /\ h e. ( D Func E ) ) -> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) = ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) )
91 90 mpoeq3dva 
 |-  ( ph -> ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) = ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) )
92 45 91 opeq12d 
 |-  ( ph -> <. ( g e. ( D Func E ) |-> ( g ( 1st ` ( <. C , D >. o.F E ) ) F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a ( <. g , F >. ( 2nd ` ( <. C , D >. o.F E ) ) <. h , F >. ) ( ( Id ` Q ) ` F ) ) ) ) >. = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. )
93 22 92 eqtrd 
 |-  ( ph -> K = <. ( g e. ( D Func E ) |-> ( g o.func F ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( x e. ( Base ` C ) |-> ( a ` ( ( 1st ` F ) ` x ) ) ) ) ) >. )