This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem curf1cl

Description: The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curfval.g 
|- G = ( <. C , D >. curryF F )
curfval.a 
|- A = ( Base ` C )
curfval.c 
|- ( ph -> C e. Cat )
curfval.d 
|- ( ph -> D e. Cat )
curfval.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
curfval.b 
|- B = ( Base ` D )
curf1.x 
|- ( ph -> X e. A )
curf1.k 
|- K = ( ( 1st ` G ) ` X )
Assertion curf1cl 
|- ( ph -> K e. ( D Func E ) )

Proof

Step Hyp Ref Expression
1 curfval.g 
 |-  G = ( <. C , D >. curryF F )
2 curfval.a 
 |-  A = ( Base ` C )
3 curfval.c 
 |-  ( ph -> C e. Cat )
4 curfval.d 
 |-  ( ph -> D e. Cat )
5 curfval.f 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
6 curfval.b 
 |-  B = ( Base ` D )
7 curf1.x 
 |-  ( ph -> X e. A )
8 curf1.k 
 |-  K = ( ( 1st ` G ) ` X )
9 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
10 eqid 
 |-  ( Id ` C ) = ( Id ` C )
11 1 2 3 4 5 6 7 8 9 10 curf1 
 |-  ( ph -> K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. )
12 6 fvexi 
 |-  B e. _V
13 12 mptex 
 |-  ( y e. B |-> ( X ( 1st ` F ) y ) ) e. _V
14 12 12 mpoex 
 |-  ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) e. _V
15 13 14 op1std 
 |-  ( K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` F ) y ) ) )
16 11 15 syl 
 |-  ( ph -> ( 1st ` K ) = ( y e. B |-> ( X ( 1st ` F ) y ) ) )
17 13 14 op2ndd 
 |-  ( K = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) )
18 11 17 syl 
 |-  ( ph -> ( 2nd ` K ) = ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) )
19 16 18 opeq12d 
 |-  ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. = <. ( y e. B |-> ( X ( 1st ` F ) y ) ) , ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) >. )
20 11 19 eqtr4d 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
21 eqid 
 |-  ( Base ` E ) = ( Base ` E )
22 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
23 eqid 
 |-  ( Id ` D ) = ( Id ` D )
24 eqid 
 |-  ( Id ` E ) = ( Id ` E )
25 eqid 
 |-  ( comp ` D ) = ( comp ` D )
26 eqid 
 |-  ( comp ` E ) = ( comp ` E )
27 funcrcl 
 |-  ( F e. ( ( C Xc. D ) Func E ) -> ( ( C Xc. D ) e. Cat /\ E e. Cat ) )
28 5 27 syl 
 |-  ( ph -> ( ( C Xc. D ) e. Cat /\ E e. Cat ) )
29 28 simprd 
 |-  ( ph -> E e. Cat )
30 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
31 30 2 6 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
32 relfunc 
 |-  Rel ( ( C Xc. D ) Func E )
33 1st2ndbr 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ F e. ( ( C Xc. D ) Func E ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
34 32 5 33 sylancr 
 |-  ( ph -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
35 31 21 34 funcf1 
 |-  ( ph -> ( 1st ` F ) : ( A X. B ) --> ( Base ` E ) )
36 35 adantr 
 |-  ( ( ph /\ y e. B ) -> ( 1st ` F ) : ( A X. B ) --> ( Base ` E ) )
37 7 adantr 
 |-  ( ( ph /\ y e. B ) -> X e. A )
38 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
39 36 37 38 fovcdmd 
 |-  ( ( ph /\ y e. B ) -> ( X ( 1st ` F ) y ) e. ( Base ` E ) )
40 16 39 fmpt3d 
 |-  ( ph -> ( 1st ` K ) : B --> ( Base ` E ) )
41 eqid 
 |-  ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) = ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) )
42 ovex 
 |-  ( y ( Hom ` D ) z ) e. _V
43 42 mptex 
 |-  ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) e. _V
44 41 43 fnmpoi 
 |-  ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) Fn ( B X. B )
45 18 fneq1d 
 |-  ( ph -> ( ( 2nd ` K ) Fn ( B X. B ) <-> ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) Fn ( B X. B ) ) )
46 44 45 mpbiri 
 |-  ( ph -> ( 2nd ` K ) Fn ( B X. B ) )
47 18 oveqd 
 |-  ( ph -> ( y ( 2nd ` K ) z ) = ( y ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) z ) )
48 41 ovmpt4g 
 |-  ( ( y e. B /\ z e. B /\ ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) e. _V ) -> ( y ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) z ) = ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) )
49 43 48 mp3an3 
 |-  ( ( y e. B /\ z e. B ) -> ( y ( y e. B , z e. B |-> ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) ) z ) = ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) )
50 47 49 sylan9eq 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( 2nd ` K ) z ) = ( g e. ( y ( Hom ` D ) z ) |-> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) ) )
51 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
52 34 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
53 7 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> X e. A )
54 simplrl 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> y e. B )
55 53 54 opelxpd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> <. X , y >. e. ( A X. B ) )
56 simplrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> z e. B )
57 53 56 opelxpd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> <. X , z >. e. ( A X. B ) )
58 31 51 22 52 55 57 funcf2 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( <. X , y >. ( 2nd ` F ) <. X , z >. ) : ( <. X , y >. ( Hom ` ( C Xc. D ) ) <. X , z >. ) --> ( ( ( 1st ` F ) ` <. X , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. X , z >. ) ) )
59 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
60 30 31 59 9 51 55 57 xpchom 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( <. X , y >. ( Hom ` ( C Xc. D ) ) <. X , z >. ) = ( ( ( 1st ` <. X , y >. ) ( Hom ` C ) ( 1st ` <. X , z >. ) ) X. ( ( 2nd ` <. X , y >. ) ( Hom ` D ) ( 2nd ` <. X , z >. ) ) ) )
61 3 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> C e. Cat )
62 4 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> D e. Cat )
63 5 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> F e. ( ( C Xc. D ) Func E ) )
64 1 2 61 62 63 6 53 8 54 curf11 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` K ) ` y ) = ( X ( 1st ` F ) y ) )
65 df-ov 
 |-  ( X ( 1st ` F ) y ) = ( ( 1st ` F ) ` <. X , y >. )
66 64 65 eqtr2di 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` F ) ` <. X , y >. ) = ( ( 1st ` K ) ` y ) )
67 1 2 61 62 63 6 53 8 56 curf11 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` K ) ` z ) = ( X ( 1st ` F ) z ) )
68 df-ov 
 |-  ( X ( 1st ` F ) z ) = ( ( 1st ` F ) ` <. X , z >. )
69 67 68 eqtr2di 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` F ) ` <. X , z >. ) = ( ( 1st ` K ) ` z ) )
70 66 69 oveq12d 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( 1st ` F ) ` <. X , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. X , z >. ) ) = ( ( ( 1st ` K ) ` y ) ( Hom ` E ) ( ( 1st ` K ) ` z ) ) )
71 60 70 feq23d 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , z >. ) : ( <. X , y >. ( Hom ` ( C Xc. D ) ) <. X , z >. ) --> ( ( ( 1st ` F ) ` <. X , y >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. X , z >. ) ) <-> ( <. X , y >. ( 2nd ` F ) <. X , z >. ) : ( ( ( 1st ` <. X , y >. ) ( Hom ` C ) ( 1st ` <. X , z >. ) ) X. ( ( 2nd ` <. X , y >. ) ( Hom ` D ) ( 2nd ` <. X , z >. ) ) ) --> ( ( ( 1st ` K ) ` y ) ( Hom ` E ) ( ( 1st ` K ) ` z ) ) ) )
72 58 71 mpbid 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( <. X , y >. ( 2nd ` F ) <. X , z >. ) : ( ( ( 1st ` <. X , y >. ) ( Hom ` C ) ( 1st ` <. X , z >. ) ) X. ( ( 2nd ` <. X , y >. ) ( Hom ` D ) ( 2nd ` <. X , z >. ) ) ) --> ( ( ( 1st ` K ) ` y ) ( Hom ` E ) ( ( 1st ` K ) ` z ) ) )
73 2 59 10 61 53 catidcl 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
74 op1stg 
 |-  ( ( X e. A /\ y e. B ) -> ( 1st ` <. X , y >. ) = X )
75 53 54 74 syl2anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 1st ` <. X , y >. ) = X )
76 op1stg 
 |-  ( ( X e. A /\ z e. B ) -> ( 1st ` <. X , z >. ) = X )
77 53 56 76 syl2anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 1st ` <. X , z >. ) = X )
78 75 77 oveq12d 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 1st ` <. X , y >. ) ( Hom ` C ) ( 1st ` <. X , z >. ) ) = ( X ( Hom ` C ) X ) )
79 73 78 eleqtrrd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( Id ` C ) ` X ) e. ( ( 1st ` <. X , y >. ) ( Hom ` C ) ( 1st ` <. X , z >. ) ) )
80 simpr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> g e. ( y ( Hom ` D ) z ) )
81 op2ndg 
 |-  ( ( X e. A /\ y e. B ) -> ( 2nd ` <. X , y >. ) = y )
82 53 54 81 syl2anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 2nd ` <. X , y >. ) = y )
83 op2ndg 
 |-  ( ( X e. A /\ z e. B ) -> ( 2nd ` <. X , z >. ) = z )
84 53 56 83 syl2anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( 2nd ` <. X , z >. ) = z )
85 82 84 oveq12d 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( 2nd ` <. X , y >. ) ( Hom ` D ) ( 2nd ` <. X , z >. ) ) = ( y ( Hom ` D ) z ) )
86 80 85 eleqtrrd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> g e. ( ( 2nd ` <. X , y >. ) ( Hom ` D ) ( 2nd ` <. X , z >. ) ) )
87 72 79 86 fovcdmd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ g e. ( y ( Hom ` D ) z ) ) -> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) e. ( ( ( 1st ` K ) ` y ) ( Hom ` E ) ( ( 1st ` K ) ` z ) ) )
88 50 87 fmpt3d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( 2nd ` K ) z ) : ( y ( Hom ` D ) z ) --> ( ( ( 1st ` K ) ` y ) ( Hom ` E ) ( ( 1st ` K ) ` z ) ) )
89 3 adantr 
 |-  ( ( ph /\ y e. B ) -> C e. Cat )
90 4 adantr 
 |-  ( ( ph /\ y e. B ) -> D e. Cat )
91 eqid 
 |-  ( Id ` ( C Xc. D ) ) = ( Id ` ( C Xc. D ) )
92 30 89 90 2 6 10 23 91 37 38 xpcid 
 |-  ( ( ph /\ y e. B ) -> ( ( Id ` ( C Xc. D ) ) ` <. X , y >. ) = <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` y ) >. )
93 92 fveq2d 
 |-  ( ( ph /\ y e. B ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ` ( ( Id ` ( C Xc. D ) ) ` <. X , y >. ) ) = ( ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ` <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` y ) >. ) )
94 df-ov 
 |-  ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ( ( Id ` D ) ` y ) ) = ( ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ` <. ( ( Id ` C ) ` X ) , ( ( Id ` D ) ` y ) >. )
95 93 94 eqtr4di 
 |-  ( ( ph /\ y e. B ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ` ( ( Id ` ( C Xc. D ) ) ` <. X , y >. ) ) = ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ( ( Id ` D ) ` y ) ) )
96 34 adantr 
 |-  ( ( ph /\ y e. B ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
97 opelxpi 
 |-  ( ( X e. A /\ y e. B ) -> <. X , y >. e. ( A X. B ) )
98 7 97 sylan 
 |-  ( ( ph /\ y e. B ) -> <. X , y >. e. ( A X. B ) )
99 31 91 24 96 98 funcid 
 |-  ( ( ph /\ y e. B ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ` ( ( Id ` ( C Xc. D ) ) ` <. X , y >. ) ) = ( ( Id ` E ) ` ( ( 1st ` F ) ` <. X , y >. ) ) )
100 95 99 eqtr3d 
 |-  ( ( ph /\ y e. B ) -> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ( ( Id ` D ) ` y ) ) = ( ( Id ` E ) ` ( ( 1st ` F ) ` <. X , y >. ) ) )
101 5 adantr 
 |-  ( ( ph /\ y e. B ) -> F e. ( ( C Xc. D ) Func E ) )
102 6 9 23 90 38 catidcl 
 |-  ( ( ph /\ y e. B ) -> ( ( Id ` D ) ` y ) e. ( y ( Hom ` D ) y ) )
103 1 2 89 90 101 6 37 8 38 9 10 38 102 curf12 
 |-  ( ( ph /\ y e. B ) -> ( ( y ( 2nd ` K ) y ) ` ( ( Id ` D ) ` y ) ) = ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , y >. ) ( ( Id ` D ) ` y ) ) )
104 1 2 89 90 101 6 37 8 38 curf11 
 |-  ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = ( X ( 1st ` F ) y ) )
105 104 65 eqtrdi 
 |-  ( ( ph /\ y e. B ) -> ( ( 1st ` K ) ` y ) = ( ( 1st ` F ) ` <. X , y >. ) )
106 105 fveq2d 
 |-  ( ( ph /\ y e. B ) -> ( ( Id ` E ) ` ( ( 1st ` K ) ` y ) ) = ( ( Id ` E ) ` ( ( 1st ` F ) ` <. X , y >. ) ) )
107 100 103 106 3eqtr4d 
 |-  ( ( ph /\ y e. B ) -> ( ( y ( 2nd ` K ) y ) ` ( ( Id ` D ) ` y ) ) = ( ( Id ` E ) ` ( ( 1st ` K ) ` y ) ) )
108 7 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> X e. A )
109 simp21 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> y e. B )
110 simp22 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> z e. B )
111 eqid 
 |-  ( comp ` C ) = ( comp ` C )
112 eqid 
 |-  ( comp ` ( C Xc. D ) ) = ( comp ` ( C Xc. D ) )
113 simp23 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> w e. B )
114 3 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> C e. Cat )
115 2 59 10 114 108 catidcl 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
116 simp3l 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> g e. ( y ( Hom ` D ) z ) )
117 simp3r 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> h e. ( z ( Hom ` D ) w ) )
118 30 2 6 59 9 108 109 108 110 111 25 112 108 113 115 116 115 117 xpcco2 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( <. ( ( Id ` C ) ` X ) , h >. ( <. <. X , y >. , <. X , z >. >. ( comp ` ( C Xc. D ) ) <. X , w >. ) <. ( ( Id ` C ) ` X ) , g >. ) = <. ( ( ( Id ` C ) ` X ) ( <. X , X >. ( comp ` C ) X ) ( ( Id ` C ) ` X ) ) , ( h ( <. y , z >. ( comp ` D ) w ) g ) >. )
119 2 59 10 114 108 111 108 115 catlid 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( ( Id ` C ) ` X ) ( <. X , X >. ( comp ` C ) X ) ( ( Id ` C ) ` X ) ) = ( ( Id ` C ) ` X ) )
120 119 opeq1d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( ( Id ` C ) ` X ) ( <. X , X >. ( comp ` C ) X ) ( ( Id ` C ) ` X ) ) , ( h ( <. y , z >. ( comp ` D ) w ) g ) >. = <. ( ( Id ` C ) ` X ) , ( h ( <. y , z >. ( comp ` D ) w ) g ) >. )
121 118 120 eqtrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( <. ( ( Id ` C ) ` X ) , h >. ( <. <. X , y >. , <. X , z >. >. ( comp ` ( C Xc. D ) ) <. X , w >. ) <. ( ( Id ` C ) ` X ) , g >. ) = <. ( ( Id ` C ) ` X ) , ( h ( <. y , z >. ( comp ` D ) w ) g ) >. )
122 121 fveq2d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ` ( <. ( ( Id ` C ) ` X ) , h >. ( <. <. X , y >. , <. X , z >. >. ( comp ` ( C Xc. D ) ) <. X , w >. ) <. ( ( Id ` C ) ` X ) , g >. ) ) = ( ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , ( h ( <. y , z >. ( comp ` D ) w ) g ) >. ) )
123 df-ov 
 |-  ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ( h ( <. y , z >. ( comp ` D ) w ) g ) ) = ( ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , ( h ( <. y , z >. ( comp ` D ) w ) g ) >. )
124 122 123 eqtr4di 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ` ( <. ( ( Id ` C ) ` X ) , h >. ( <. <. X , y >. , <. X , z >. >. ( comp ` ( C Xc. D ) ) <. X , w >. ) <. ( ( Id ` C ) ` X ) , g >. ) ) = ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ( h ( <. y , z >. ( comp ` D ) w ) g ) ) )
125 34 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
126 108 109 opelxpd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. X , y >. e. ( A X. B ) )
127 108 110 opelxpd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. X , z >. e. ( A X. B ) )
128 108 113 opelxpd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. X , w >. e. ( A X. B ) )
129 115 116 opelxpd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` X ) , g >. e. ( ( X ( Hom ` C ) X ) X. ( y ( Hom ` D ) z ) ) )
130 30 2 6 59 9 108 109 108 110 51 xpchom2 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( <. X , y >. ( Hom ` ( C Xc. D ) ) <. X , z >. ) = ( ( X ( Hom ` C ) X ) X. ( y ( Hom ` D ) z ) ) )
131 129 130 eleqtrrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` X ) , g >. e. ( <. X , y >. ( Hom ` ( C Xc. D ) ) <. X , z >. ) )
132 115 117 opelxpd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` X ) , h >. e. ( ( X ( Hom ` C ) X ) X. ( z ( Hom ` D ) w ) ) )
133 30 2 6 59 9 108 110 108 113 51 xpchom2 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. X , w >. ) = ( ( X ( Hom ` C ) X ) X. ( z ( Hom ` D ) w ) ) )
134 132 133 eleqtrrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` X ) , h >. e. ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. X , w >. ) )
135 31 51 112 26 125 126 127 128 131 134 funcco 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ` ( <. ( ( Id ` C ) ` X ) , h >. ( <. <. X , y >. , <. X , z >. >. ( comp ` ( C Xc. D ) ) <. X , w >. ) <. ( ( Id ` C ) ` X ) , g >. ) ) = ( ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , h >. ) ( <. ( ( 1st ` F ) ` <. X , y >. ) , ( ( 1st ` F ) ` <. X , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. X , w >. ) ) ( ( <. X , y >. ( 2nd ` F ) <. X , z >. ) ` <. ( ( Id ` C ) ` X ) , g >. ) ) )
136 124 135 eqtr3d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ( h ( <. y , z >. ( comp ` D ) w ) g ) ) = ( ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , h >. ) ( <. ( ( 1st ` F ) ` <. X , y >. ) , ( ( 1st ` F ) ` <. X , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. X , w >. ) ) ( ( <. X , y >. ( 2nd ` F ) <. X , z >. ) ` <. ( ( Id ` C ) ` X ) , g >. ) ) )
137 4 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> D e. Cat )
138 5 3ad2ant1 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> F e. ( ( C Xc. D ) Func E ) )
139 6 9 25 137 109 110 113 116 117 catcocl 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( h ( <. y , z >. ( comp ` D ) w ) g ) e. ( y ( Hom ` D ) w ) )
140 1 2 114 137 138 6 108 8 109 9 10 113 139 curf12 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( y ( 2nd ` K ) w ) ` ( h ( <. y , z >. ( comp ` D ) w ) g ) ) = ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , w >. ) ( h ( <. y , z >. ( comp ` D ) w ) g ) ) )
141 1 2 114 137 138 6 108 8 109 curf11 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` K ) ` y ) = ( X ( 1st ` F ) y ) )
142 141 65 eqtrdi 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` K ) ` y ) = ( ( 1st ` F ) ` <. X , y >. ) )
143 1 2 114 137 138 6 108 8 110 curf11 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` K ) ` z ) = ( X ( 1st ` F ) z ) )
144 143 68 eqtrdi 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` K ) ` z ) = ( ( 1st ` F ) ` <. X , z >. ) )
145 142 144 opeq12d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( 1st ` K ) ` y ) , ( ( 1st ` K ) ` z ) >. = <. ( ( 1st ` F ) ` <. X , y >. ) , ( ( 1st ` F ) ` <. X , z >. ) >. )
146 1 2 114 137 138 6 108 8 113 curf11 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` K ) ` w ) = ( X ( 1st ` F ) w ) )
147 df-ov 
 |-  ( X ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. X , w >. )
148 146 147 eqtrdi 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` K ) ` w ) = ( ( 1st ` F ) ` <. X , w >. ) )
149 145 148 oveq12d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( <. ( ( 1st ` K ) ` y ) , ( ( 1st ` K ) ` z ) >. ( comp ` E ) ( ( 1st ` K ) ` w ) ) = ( <. ( ( 1st ` F ) ` <. X , y >. ) , ( ( 1st ` F ) ` <. X , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. X , w >. ) ) )
150 1 2 114 137 138 6 108 8 110 9 10 113 117 curf12 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( z ( 2nd ` K ) w ) ` h ) = ( ( ( Id ` C ) ` X ) ( <. X , z >. ( 2nd ` F ) <. X , w >. ) h ) )
151 df-ov 
 |-  ( ( ( Id ` C ) ` X ) ( <. X , z >. ( 2nd ` F ) <. X , w >. ) h ) = ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , h >. )
152 150 151 eqtrdi 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( z ( 2nd ` K ) w ) ` h ) = ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , h >. ) )
153 1 2 114 137 138 6 108 8 109 9 10 110 116 curf12 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( y ( 2nd ` K ) z ) ` g ) = ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) )
154 df-ov 
 |-  ( ( ( Id ` C ) ` X ) ( <. X , y >. ( 2nd ` F ) <. X , z >. ) g ) = ( ( <. X , y >. ( 2nd ` F ) <. X , z >. ) ` <. ( ( Id ` C ) ` X ) , g >. )
155 153 154 eqtrdi 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( y ( 2nd ` K ) z ) ` g ) = ( ( <. X , y >. ( 2nd ` F ) <. X , z >. ) ` <. ( ( Id ` C ) ` X ) , g >. ) )
156 149 152 155 oveq123d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( ( z ( 2nd ` K ) w ) ` h ) ( <. ( ( 1st ` K ) ` y ) , ( ( 1st ` K ) ` z ) >. ( comp ` E ) ( ( 1st ` K ) ` w ) ) ( ( y ( 2nd ` K ) z ) ` g ) ) = ( ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , h >. ) ( <. ( ( 1st ` F ) ` <. X , y >. ) , ( ( 1st ` F ) ` <. X , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. X , w >. ) ) ( ( <. X , y >. ( 2nd ` F ) <. X , z >. ) ` <. ( ( Id ` C ) ` X ) , g >. ) ) )
157 136 140 156 3eqtr4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B /\ w e. B ) /\ ( g e. ( y ( Hom ` D ) z ) /\ h e. ( z ( Hom ` D ) w ) ) ) -> ( ( y ( 2nd ` K ) w ) ` ( h ( <. y , z >. ( comp ` D ) w ) g ) ) = ( ( ( z ( 2nd ` K ) w ) ` h ) ( <. ( ( 1st ` K ) ` y ) , ( ( 1st ` K ) ` z ) >. ( comp ` E ) ( ( 1st ` K ) ` w ) ) ( ( y ( 2nd ` K ) z ) ` g ) ) )
158 6 21 9 22 23 24 25 26 4 29 40 46 88 107 157 isfuncd 
 |-  ( ph -> ( 1st ` K ) ( D Func E ) ( 2nd ` K ) )
159 df-br 
 |-  ( ( 1st ` K ) ( D Func E ) ( 2nd ` K ) <-> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( D Func E ) )
160 158 159 sylib 
 |-  ( ph -> <. ( 1st ` K ) , ( 2nd ` K ) >. e. ( D Func E ) )
161 20 160 eqeltrd 
 |-  ( ph -> K e. ( D Func E ) )