Metamath Proof Explorer

Theorem 1st2ndprf

Description: Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses 1st2ndprf.t 
|- T = ( D Xc. E )
1st2ndprf.f 
|- ( ph -> F e. ( C Func T ) )
1st2ndprf.d 
|- ( ph -> D e. Cat )
1st2ndprf.e 
|- ( ph -> E e. Cat )
Assertion 1st2ndprf 
|- ( ph -> F = ( ( ( D 1stF E ) o.func F ) pairF ( ( D 2ndF E ) o.func F ) ) )

Proof

Step Hyp Ref Expression
1 1st2ndprf.t 
 |-  T = ( D Xc. E )
2 1st2ndprf.f 
 |-  ( ph -> F e. ( C Func T ) )
3 1st2ndprf.d 
 |-  ( ph -> D e. Cat )
4 1st2ndprf.e 
 |-  ( ph -> E e. Cat )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 1 6 7 xpcbas 
 |-  ( ( Base ` D ) X. ( Base ` E ) ) = ( Base ` T )
9 relfunc 
 |-  Rel ( C Func T )
10 1st2ndbr 
 |-  ( ( Rel ( C Func T ) /\ F e. ( C Func T ) ) -> ( 1st ` F ) ( C Func T ) ( 2nd ` F ) )
11 9 2 10 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func T ) ( 2nd ` F ) )
12 5 8 11 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( ( Base ` D ) X. ( Base ` E ) ) )
13 12 feqmptd 
 |-  ( ph -> ( 1st ` F ) = ( x e. ( Base ` C ) |-> ( ( 1st ` F ) ` x ) ) )
14 12 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
15 1st2nd2 
 |-  ( ( ( 1st ` F ) ` x ) e. ( ( Base ` D ) X. ( Base ` E ) ) -> ( ( 1st ` F ) ` x ) = <. ( 1st ` ( ( 1st ` F ) ` x ) ) , ( 2nd ` ( ( 1st ` F ) ` x ) ) >. )
16 14 15 syl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) = <. ( 1st ` ( ( 1st ` F ) ` x ) ) , ( 2nd ` ( ( 1st ` F ) ` x ) ) >. )
17 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F e. ( C Func T ) )
18 eqid 
 |-  ( D 1stF E ) = ( D 1stF E )
19 1 3 4 18 1stfcl 
 |-  ( ph -> ( D 1stF E ) e. ( T Func D ) )
20 19 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( D 1stF E ) e. ( T Func D ) )
21 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
22 5 17 20 21 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) = ( ( 1st ` ( D 1stF E ) ) ` ( ( 1st ` F ) ` x ) ) )
23 eqid 
 |-  ( Hom ` T ) = ( Hom ` T )
24 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
25 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E e. Cat )
26 1 8 23 24 25 18 14 1stf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( D 1stF E ) ) ` ( ( 1st ` F ) ` x ) ) = ( 1st ` ( ( 1st ` F ) ` x ) ) )
27 22 26 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) = ( 1st ` ( ( 1st ` F ) ` x ) ) )
28 eqid 
 |-  ( D 2ndF E ) = ( D 2ndF E )
29 1 3 4 28 2ndfcl 
 |-  ( ph -> ( D 2ndF E ) e. ( T Func E ) )
30 29 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( D 2ndF E ) e. ( T Func E ) )
31 5 17 30 21 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) = ( ( 1st ` ( D 2ndF E ) ) ` ( ( 1st ` F ) ` x ) ) )
32 1 8 23 24 25 28 14 2ndf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( D 2ndF E ) ) ` ( ( 1st ` F ) ` x ) ) = ( 2nd ` ( ( 1st ` F ) ` x ) ) )
33 31 32 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) = ( 2nd ` ( ( 1st ` F ) ` x ) ) )
34 27 33 opeq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) , ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) >. = <. ( 1st ` ( ( 1st ` F ) ` x ) ) , ( 2nd ` ( ( 1st ` F ) ` x ) ) >. )
35 16 34 eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) = <. ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) , ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) >. )
36 35 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( 1st ` F ) ` x ) ) = ( x e. ( Base ` C ) |-> <. ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) , ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) >. ) )
37 13 36 eqtrd 
 |-  ( ph -> ( 1st ` F ) = ( x e. ( Base ` C ) |-> <. ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) , ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) >. ) )
38 5 11 funcfn2 
 |-  ( ph -> ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
39 fnov 
 |-  ( ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
40 38 39 sylib 
 |-  ( ph -> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
41 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
42 11 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` F ) ( C Func T ) ( 2nd ` F ) )
43 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
44 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
45 5 41 23 42 43 44 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) )
46 45 feqmptd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` F ) y ) ` f ) ) )
47 1 23 relxpchom 
 |-  Rel ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) )
48 45 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) )
49 1st2nd 
 |-  ( ( Rel ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) /\ ( ( x ( 2nd ` F ) y ) ` f ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) = <. ( 1st ` ( ( x ( 2nd ` F ) y ) ` f ) ) , ( 2nd ` ( ( x ( 2nd ` F ) y ) ` f ) ) >. )
50 47 48 49 sylancr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) = <. ( 1st ` ( ( x ( 2nd ` F ) y ) ` f ) ) , ( 2nd ` ( ( x ( 2nd ` F ) y ) ` f ) ) >. )
51 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> F e. ( C Func T ) )
52 19 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( D 1stF E ) e. ( T Func D ) )
53 43 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
54 44 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
55 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> f e. ( x ( Hom ` C ) y ) )
56 5 51 52 53 54 41 55 cofu2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
57 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> D e. Cat )
58 4 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E e. Cat )
59 14 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` F ) ` x ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
60 12 ffvelrnda 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( ( 1st ` F ) ` y ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
61 60 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` F ) ` y ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
62 1 8 23 57 58 18 59 61 1stf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` F ) ` y ) ) = ( 1st |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) )
63 62 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` F ) ` y ) ) = ( 1st |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) )
64 63 fveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( 1st |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
65 48 fvresd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( 1st |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) = ( 1st ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
66 56 64 65 3eqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) = ( 1st ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
67 29 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( D 2ndF E ) e. ( T Func E ) )
68 5 51 67 53 54 41 55 cofu2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) = ( ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 2ndF E ) ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
69 1 8 23 57 58 28 59 61 2ndf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 2ndF E ) ) ( ( 1st ` F ) ` y ) ) = ( 2nd |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) )
70 69 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 2ndF E ) ) ( ( 1st ` F ) ` y ) ) = ( 2nd |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) )
71 70 fveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( ( 1st ` F ) ` x ) ( 2nd ` ( D 2ndF E ) ) ( ( 1st ` F ) ` y ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) = ( ( 2nd |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
72 48 fvresd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( 2nd |` ( ( ( 1st ` F ) ` x ) ( Hom ` T ) ( ( 1st ` F ) ` y ) ) ) ` ( ( x ( 2nd ` F ) y ) ` f ) ) = ( 2nd ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
73 68 71 72 3eqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) = ( 2nd ` ( ( x ( 2nd ` F ) y ) ` f ) ) )
74 66 73 opeq12d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. = <. ( 1st ` ( ( x ( 2nd ` F ) y ) ` f ) ) , ( 2nd ` ( ( x ( 2nd ` F ) y ) ` f ) ) >. )
75 50 74 eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` F ) y ) ` f ) = <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. )
76 75 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` F ) y ) ` f ) ) = ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) )
77 46 76 eqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) = ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) )
78 77 3impb 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( 2nd ` F ) y ) = ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) )
79 78 mpoeq3dva 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) ) )
80 40 79 eqtrd 
 |-  ( ph -> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) ) )
81 37 80 opeq12d 
 |-  ( ph -> <. ( 1st ` F ) , ( 2nd ` F ) >. = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) , ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) ) >. )
82 1st2nd 
 |-  ( ( Rel ( C Func T ) /\ F e. ( C Func T ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
83 9 2 82 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
84 eqid 
 |-  ( ( ( D 1stF E ) o.func F ) pairF ( ( D 2ndF E ) o.func F ) ) = ( ( ( D 1stF E ) o.func F ) pairF ( ( D 2ndF E ) o.func F ) )
85 2 19 cofucl 
 |-  ( ph -> ( ( D 1stF E ) o.func F ) e. ( C Func D ) )
86 2 29 cofucl 
 |-  ( ph -> ( ( D 2ndF E ) o.func F ) e. ( C Func E ) )
87 84 5 41 85 86 prfval 
 |-  ( ph -> ( ( ( D 1stF E ) o.func F ) pairF ( ( D 2ndF E ) o.func F ) ) = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` ( ( D 1stF E ) o.func F ) ) ` x ) , ( ( 1st ` ( ( D 2ndF E ) o.func F ) ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( f e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` ( ( D 1stF E ) o.func F ) ) y ) ` f ) , ( ( x ( 2nd ` ( ( D 2ndF E ) o.func F ) ) y ) ` f ) >. ) ) >. )
88 81 83 87 3eqtr4d 
 |-  ( ph -> F = ( ( ( D 1stF E ) o.func F ) pairF ( ( D 2ndF E ) o.func F ) ) )