Metamath Proof Explorer

Theorem prf1st

Description: Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prf1st.p 
|- P = ( F pairF G )
prf1st.c 
|- ( ph -> F e. ( C Func D ) )
prf1st.d 
|- ( ph -> G e. ( C Func E ) )
Assertion prf1st 
|- ( ph -> ( ( D 1stF E ) o.func P ) = F )

Proof

Step Hyp Ref Expression
1 prf1st.p 
 |-  P = ( F pairF G )
2 prf1st.c 
 |-  ( ph -> F e. ( C Func D ) )
3 prf1st.d 
 |-  ( ph -> G e. ( C Func E ) )
4 eqid 
 |-  ( D Xc. E ) = ( D Xc. E )
5 eqid 
 |-  ( Base ` D ) = ( Base ` D )
6 eqid 
 |-  ( Base ` E ) = ( Base ` E )
7 4 5 6 xpcbas 
 |-  ( ( Base ` D ) X. ( Base ` E ) ) = ( Base ` ( D Xc. E ) )
8 eqid 
 |-  ( Hom ` ( D Xc. E ) ) = ( Hom ` ( D Xc. E ) )
9 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
10 2 9 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
11 10 simprd 
 |-  ( ph -> D e. Cat )
12 11 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
13 funcrcl 
 |-  ( G e. ( C Func E ) -> ( C e. Cat /\ E e. Cat ) )
14 3 13 syl 
 |-  ( ph -> ( C e. Cat /\ E e. Cat ) )
15 14 simprd 
 |-  ( ph -> E e. Cat )
16 15 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> E e. Cat )
17 eqid 
 |-  ( D 1stF E ) = ( D 1stF E )
18 eqid 
 |-  ( Base ` C ) = ( Base ` C )
19 relfunc 
 |-  Rel ( C Func D )
20 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
21 19 2 20 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
22 18 5 21 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( Base ` C ) --> ( Base ` D ) )
23 22 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
24 relfunc 
 |-  Rel ( C Func E )
25 1st2ndbr 
 |-  ( ( Rel ( C Func E ) /\ G e. ( C Func E ) ) -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
26 24 3 25 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func E ) ( 2nd ` G ) )
27 18 6 26 funcf1 
 |-  ( ph -> ( 1st ` G ) : ( Base ` C ) --> ( Base ` E ) )
28 27 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` G ) ` x ) e. ( Base ` E ) )
29 23 28 opelxpd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. e. ( ( Base ` D ) X. ( Base ` E ) ) )
30 4 7 8 12 16 17 29 1stf1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( D 1stF E ) ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) = ( 1st ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
31 fvex 
 |-  ( ( 1st ` F ) ` x ) e. _V
32 fvex 
 |-  ( ( 1st ` G ) ` x ) e. _V
33 31 32 op1st 
 |-  ( 1st ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) = ( ( 1st ` F ) ` x )
34 30 33 eqtrdi 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( D 1stF E ) ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) = ( ( 1st ` F ) ` x ) )
35 34 mpteq2dva 
 |-  ( ph -> ( x e. ( Base ` C ) |-> ( ( 1st ` ( D 1stF E ) ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) ) = ( x e. ( Base ` C ) |-> ( ( 1st ` F ) ` x ) ) )
36 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
37 1 18 36 2 3 prfval 
 |-  ( ph -> P = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
38 fvex 
 |-  ( Base ` C ) e. _V
39 38 mptex 
 |-  ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) e. _V
40 38 38 mpoex 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) e. _V
41 39 40 op1std 
 |-  ( P = <. ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( h e. ( x ( Hom ` C ) y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. -> ( 1st ` P ) = ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
42 37 41 syl 
 |-  ( ph -> ( 1st ` P ) = ( x e. ( Base ` C ) |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
43 relfunc 
 |-  Rel ( ( D Xc. E ) Func D )
44 4 11 15 17 1stfcl 
 |-  ( ph -> ( D 1stF E ) e. ( ( D Xc. E ) Func D ) )
45 1st2ndbr 
 |-  ( ( Rel ( ( D Xc. E ) Func D ) /\ ( D 1stF E ) e. ( ( D Xc. E ) Func D ) ) -> ( 1st ` ( D 1stF E ) ) ( ( D Xc. E ) Func D ) ( 2nd ` ( D 1stF E ) ) )
46 43 44 45 sylancr 
 |-  ( ph -> ( 1st ` ( D 1stF E ) ) ( ( D Xc. E ) Func D ) ( 2nd ` ( D 1stF E ) ) )
47 7 5 46 funcf1 
 |-  ( ph -> ( 1st ` ( D 1stF E ) ) : ( ( Base ` D ) X. ( Base ` E ) ) --> ( Base ` D ) )
48 47 feqmptd 
 |-  ( ph -> ( 1st ` ( D 1stF E ) ) = ( u e. ( ( Base ` D ) X. ( Base ` E ) ) |-> ( ( 1st ` ( D 1stF E ) ) ` u ) ) )
49 fveq2 
 |-  ( u = <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. -> ( ( 1st ` ( D 1stF E ) ) ` u ) = ( ( 1st ` ( D 1stF E ) ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
50 29 42 48 49 fmptco 
 |-  ( ph -> ( ( 1st ` ( D 1stF E ) ) o. ( 1st ` P ) ) = ( x e. ( Base ` C ) |-> ( ( 1st ` ( D 1stF E ) ) ` <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) ) )
51 22 feqmptd 
 |-  ( ph -> ( 1st ` F ) = ( x e. ( Base ` C ) |-> ( ( 1st ` F ) ` x ) ) )
52 35 50 51 3eqtr4d 
 |-  ( ph -> ( ( 1st ` ( D 1stF E ) ) o. ( 1st ` P ) ) = ( 1st ` F ) )
53 11 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> D e. Cat )
54 15 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> E e. Cat )
55 relfunc 
 |-  Rel ( C Func ( D Xc. E ) )
56 1 4 2 3 prfcl 
 |-  ( ph -> P e. ( C Func ( D Xc. E ) ) )
57 1st2ndbr 
 |-  ( ( Rel ( C Func ( D Xc. E ) ) /\ P e. ( C Func ( D Xc. E ) ) ) -> ( 1st ` P ) ( C Func ( D Xc. E ) ) ( 2nd ` P ) )
58 55 56 57 sylancr 
 |-  ( ph -> ( 1st ` P ) ( C Func ( D Xc. E ) ) ( 2nd ` P ) )
59 18 7 58 funcf1 
 |-  ( ph -> ( 1st ` P ) : ( Base ` C ) --> ( ( Base ` D ) X. ( Base ` E ) ) )
60 59 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` P ) ` x ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
61 60 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` P ) ` x ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
62 61 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( 1st ` P ) ` x ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
63 59 ffvelrnda 
 |-  ( ( ph /\ y e. ( Base ` C ) ) -> ( ( 1st ` P ) ` y ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
64 63 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` P ) ` y ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
65 64 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( 1st ` P ) ` y ) e. ( ( Base ` D ) X. ( Base ` E ) ) )
66 4 7 8 53 54 17 62 65 1stf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) = ( 1st |` ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) ) )
67 66 fveq1d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) = ( ( 1st |` ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) )
68 58 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` P ) ( C Func ( D Xc. E ) ) ( 2nd ` P ) )
69 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
70 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
71 18 36 8 68 69 70 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` P ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) )
72 71 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` P ) y ) ` f ) e. ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) )
73 72 fvresd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( 1st |` ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) = ( 1st ` ( ( x ( 2nd ` P ) y ) ` f ) ) )
74 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> F e. ( C Func D ) )
75 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> G e. ( C Func E ) )
76 69 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
77 70 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
78 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> f e. ( x ( Hom ` C ) y ) )
79 1 18 36 74 75 76 77 78 prf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( x ( 2nd ` P ) y ) ` f ) = <. ( ( x ( 2nd ` F ) y ) ` f ) , ( ( x ( 2nd ` G ) y ) ` f ) >. )
80 79 fveq2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( ( x ( 2nd ` P ) y ) ` f ) ) = ( 1st ` <. ( ( x ( 2nd ` F ) y ) ` f ) , ( ( x ( 2nd ` G ) y ) ` f ) >. ) )
81 fvex 
 |-  ( ( x ( 2nd ` F ) y ) ` f ) e. _V
82 fvex 
 |-  ( ( x ( 2nd ` G ) y ) ` f ) e. _V
83 81 82 op1st 
 |-  ( 1st ` <. ( ( x ( 2nd ` F ) y ) ` f ) , ( ( x ( 2nd ` G ) y ) ` f ) >. ) = ( ( x ( 2nd ` F ) y ) ` f )
84 80 83 eqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 1st ` ( ( x ( 2nd ` P ) y ) ` f ) ) = ( ( x ( 2nd ` F ) y ) ` f ) )
85 67 73 84 3eqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) = ( ( x ( 2nd ` F ) y ) ` f ) )
86 85 mpteq2dva 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( f e. ( x ( Hom ` C ) y ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( x ( 2nd ` F ) y ) ` f ) ) )
87 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
88 46 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( D 1stF E ) ) ( ( D Xc. E ) Func D ) ( 2nd ` ( D 1stF E ) ) )
89 7 8 87 88 61 64 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) : ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) --> ( ( ( 1st ` ( D 1stF E ) ) ` ( ( 1st ` P ) ` x ) ) ( Hom ` D ) ( ( 1st ` ( D 1stF E ) ) ` ( ( 1st ` P ) ` y ) ) ) )
90 fcompt 
 |-  ( ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) : ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) --> ( ( ( 1st ` ( D 1stF E ) ) ` ( ( 1st ` P ) ` x ) ) ( Hom ` D ) ( ( 1st ` ( D 1stF E ) ) ` ( ( 1st ` P ) ` y ) ) ) /\ ( x ( 2nd ` P ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` P ) ` x ) ( Hom ` ( D Xc. E ) ) ( ( 1st ` P ) ` y ) ) ) -> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) ) )
91 89 71 90 syl2anc 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) = ( f e. ( x ( Hom ` C ) y ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) ` ( ( x ( 2nd ` P ) y ) ` f ) ) ) )
92 21 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
93 18 36 87 92 69 70 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` F ) y ) : ( x ( Hom ` C ) y ) --> ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` y ) ) )
94 93 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 ) ) )
95 86 91 94 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) = ( x ( 2nd ` F ) y ) )
96 95 3impb 
 |-  ( ( ph /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) = ( x ( 2nd ` F ) y ) )
97 96 mpoeq3dva 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
98 18 21 funcfn2 
 |-  ( ph -> ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
99 fnov 
 |-  ( ( 2nd ` F ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
100 98 99 sylib 
 |-  ( ph -> ( 2nd ` F ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( 2nd ` F ) y ) ) )
101 97 100 eqtr4d 
 |-  ( ph -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) ) = ( 2nd ` F ) )
102 52 101 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( D 1stF E ) ) o. ( 1st ` P ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) ) >. = <. ( 1st ` F ) , ( 2nd ` F ) >. )
103 18 56 44 cofuval 
 |-  ( ph -> ( ( D 1stF E ) o.func P ) = <. ( ( 1st ` ( D 1stF E ) ) o. ( 1st ` P ) ) , ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( ( ( 1st ` P ) ` x ) ( 2nd ` ( D 1stF E ) ) ( ( 1st ` P ) ` y ) ) o. ( x ( 2nd ` P ) y ) ) ) >. )
104 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
105 19 2 104 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
106 102 103 105 3eqtr4d 
 |-  ( ph -> ( ( D 1stF E ) o.func P ) = F )