Metamath Proof Explorer

Theorem curf2cl

Description: The curry functor at a morphism is a natural transformation. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curf2.g 
|- G = ( <. C , D >. curryF F )
curf2.a 
|- A = ( Base ` C )
curf2.c 
|- ( ph -> C e. Cat )
curf2.d 
|- ( ph -> D e. Cat )
curf2.f 
|- ( ph -> F e. ( ( C Xc. D ) Func E ) )
curf2.b 
|- B = ( Base ` D )
curf2.h 
|- H = ( Hom ` C )
curf2.i 
|- I = ( Id ` D )
curf2.x 
|- ( ph -> X e. A )
curf2.y 
|- ( ph -> Y e. A )
curf2.k 
|- ( ph -> K e. ( X H Y ) )
curf2.l 
|- L = ( ( X ( 2nd ` G ) Y ) ` K )
curf2.n 
|- N = ( D Nat E )
Assertion curf2cl 
|- ( ph -> L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) )

Proof

Step Hyp Ref Expression
1 curf2.g 
 |-  G = ( <. C , D >. curryF F )
2 curf2.a 
 |-  A = ( Base ` C )
3 curf2.c 
 |-  ( ph -> C e. Cat )
4 curf2.d 
 |-  ( ph -> D e. Cat )
5 curf2.f 
 |-  ( ph -> F e. ( ( C Xc. D ) Func E ) )
6 curf2.b 
 |-  B = ( Base ` D )
7 curf2.h 
 |-  H = ( Hom ` C )
8 curf2.i 
 |-  I = ( Id ` D )
9 curf2.x 
 |-  ( ph -> X e. A )
10 curf2.y 
 |-  ( ph -> Y e. A )
11 curf2.k 
 |-  ( ph -> K e. ( X H Y ) )
12 curf2.l 
 |-  L = ( ( X ( 2nd ` G ) Y ) ` K )
13 curf2.n 
 |-  N = ( D Nat E )
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 
 |-  ( ph -> L = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) )
15 eqid 
 |-  ( C Xc. D ) = ( C Xc. D )
16 15 2 6 xpcbas 
 |-  ( A X. B ) = ( Base ` ( C Xc. D ) )
17 eqid 
 |-  ( Hom ` ( C Xc. D ) ) = ( Hom ` ( C Xc. D ) )
18 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
19 relfunc 
 |-  Rel ( ( C Xc. D ) Func E )
20 1st2ndbr 
 |-  ( ( Rel ( ( C Xc. D ) Func E ) /\ F e. ( ( C Xc. D ) Func E ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
21 19 5 20 sylancr 
 |-  ( ph -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
22 21 adantr 
 |-  ( ( ph /\ z e. B ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
23 opelxpi 
 |-  ( ( X e. A /\ z e. B ) -> <. X , z >. e. ( A X. B ) )
24 9 23 sylan 
 |-  ( ( ph /\ z e. B ) -> <. X , z >. e. ( A X. B ) )
25 opelxpi 
 |-  ( ( Y e. A /\ z e. B ) -> <. Y , z >. e. ( A X. B ) )
26 10 25 sylan 
 |-  ( ( ph /\ z e. B ) -> <. Y , z >. e. ( A X. B ) )
27 16 17 18 22 24 26 funcf2 
 |-  ( ( ph /\ z e. B ) -> ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) : ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. Y , z >. ) --> ( ( ( 1st ` F ) ` <. X , z >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. Y , z >. ) ) )
28 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
29 9 adantr 
 |-  ( ( ph /\ z e. B ) -> X e. A )
30 simpr 
 |-  ( ( ph /\ z e. B ) -> z e. B )
31 10 adantr 
 |-  ( ( ph /\ z e. B ) -> Y e. A )
32 15 2 6 7 28 29 30 31 30 17 xpchom2 
 |-  ( ( ph /\ z e. B ) -> ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. Y , z >. ) = ( ( X H Y ) X. ( z ( Hom ` D ) z ) ) )
33 32 feq2d 
 |-  ( ( ph /\ z e. B ) -> ( ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) : ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. Y , z >. ) --> ( ( ( 1st ` F ) ` <. X , z >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. Y , z >. ) ) <-> ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) : ( ( X H Y ) X. ( z ( Hom ` D ) z ) ) --> ( ( ( 1st ` F ) ` <. X , z >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. Y , z >. ) ) ) )
34 27 33 mpbid 
 |-  ( ( ph /\ z e. B ) -> ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) : ( ( X H Y ) X. ( z ( Hom ` D ) z ) ) --> ( ( ( 1st ` F ) ` <. X , z >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. Y , z >. ) ) )
35 11 adantr 
 |-  ( ( ph /\ z e. B ) -> K e. ( X H Y ) )
36 4 adantr 
 |-  ( ( ph /\ z e. B ) -> D e. Cat )
37 6 28 8 36 30 catidcl 
 |-  ( ( ph /\ z e. B ) -> ( I ` z ) e. ( z ( Hom ` D ) z ) )
38 34 35 37 fovrnd 
 |-  ( ( ph /\ z e. B ) -> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) e. ( ( ( 1st ` F ) ` <. X , z >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. Y , z >. ) ) )
39 3 adantr 
 |-  ( ( ph /\ z e. B ) -> C e. Cat )
40 5 adantr 
 |-  ( ( ph /\ z e. B ) -> F e. ( ( C Xc. D ) Func E ) )
41 eqid 
 |-  ( ( 1st ` G ) ` X ) = ( ( 1st ` G ) ` X )
42 1 2 39 36 40 6 29 41 30 curf11 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) = ( X ( 1st ` F ) z ) )
43 df-ov 
 |-  ( X ( 1st ` F ) z ) = ( ( 1st ` F ) ` <. X , z >. )
44 42 43 eqtrdi 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) = ( ( 1st ` F ) ` <. X , z >. ) )
45 eqid 
 |-  ( ( 1st ` G ) ` Y ) = ( ( 1st ` G ) ` Y )
46 1 2 39 36 40 6 31 45 30 curf11 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) = ( Y ( 1st ` F ) z ) )
47 df-ov 
 |-  ( Y ( 1st ` F ) z ) = ( ( 1st ` F ) ` <. Y , z >. )
48 46 47 eqtrdi 
 |-  ( ( ph /\ z e. B ) -> ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) = ( ( 1st ` F ) ` <. Y , z >. ) )
49 44 48 oveq12d 
 |-  ( ( ph /\ z e. B ) -> ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) = ( ( ( 1st ` F ) ` <. X , z >. ) ( Hom ` E ) ( ( 1st ` F ) ` <. Y , z >. ) ) )
50 38 49 eleqtrrd 
 |-  ( ( ph /\ z e. B ) -> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) e. ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) )
51 50 ralrimiva 
 |-  ( ph -> A. z e. B ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) e. ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) )
52 6 fvexi 
 |-  B e. _V
53 mptelixpg 
 |-  ( B e. _V -> ( ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) <-> A. z e. B ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) e. ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) ) )
54 52 53 ax-mp 
 |-  ( ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) <-> A. z e. B ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) e. ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) )
55 51 54 sylibr 
 |-  ( ph -> ( z e. B |-> ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) ) e. X_ z e. B ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) )
56 14 55 eqeltrd 
 |-  ( ph -> L e. X_ z e. B ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) )
57 eqid 
 |-  ( Id ` C ) = ( Id ` C )
58 3 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> C e. Cat )
59 9 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> X e. A )
60 eqid 
 |-  ( comp ` C ) = ( comp ` C )
61 10 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> Y e. A )
62 11 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> K e. ( X H Y ) )
63 2 7 57 58 59 60 61 62 catrid 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( K ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) = K )
64 2 7 57 58 59 60 61 62 catlid 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) K ) = K )
65 63 64 eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( K ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) = ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) K ) )
66 4 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> D e. Cat )
67 simpr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> z e. B )
68 eqid 
 |-  ( comp ` D ) = ( comp ` D )
69 simpr2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> w e. B )
70 simpr3 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> f e. ( z ( Hom ` D ) w ) )
71 6 28 8 66 67 68 69 70 catlid 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( I ` w ) ( <. z , w >. ( comp ` D ) w ) f ) = f )
72 6 28 8 66 67 68 69 70 catrid 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( f ( <. z , z >. ( comp ` D ) w ) ( I ` z ) ) = f )
73 71 72 eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( I ` w ) ( <. z , w >. ( comp ` D ) w ) f ) = ( f ( <. z , z >. ( comp ` D ) w ) ( I ` z ) ) )
74 65 73 opeq12d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( K ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) , ( ( I ` w ) ( <. z , w >. ( comp ` D ) w ) f ) >. = <. ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) K ) , ( f ( <. z , z >. ( comp ` D ) w ) ( I ` z ) ) >. )
75 eqid 
 |-  ( comp ` ( C Xc. D ) ) = ( comp ` ( C Xc. D ) )
76 2 7 57 58 59 catidcl 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( Id ` C ) ` X ) e. ( X H X ) )
77 6 28 8 66 69 catidcl 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( I ` w ) e. ( w ( Hom ` D ) w ) )
78 15 2 6 7 28 59 67 59 69 60 68 75 61 69 76 70 62 77 xpcco2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. K , ( I ` w ) >. ( <. <. X , z >. , <. X , w >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. ( ( Id ` C ) ` X ) , f >. ) = <. ( K ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) , ( ( I ` w ) ( <. z , w >. ( comp ` D ) w ) f ) >. )
79 37 3ad2antr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( I ` z ) e. ( z ( Hom ` D ) z ) )
80 2 7 57 58 61 catidcl 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( Id ` C ) ` Y ) e. ( Y H Y ) )
81 15 2 6 7 28 59 67 61 67 60 68 75 61 69 62 79 80 70 xpcco2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. ( ( Id ` C ) ` Y ) , f >. ( <. <. X , z >. , <. Y , z >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. K , ( I ` z ) >. ) = <. ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) K ) , ( f ( <. z , z >. ( comp ` D ) w ) ( I ` z ) ) >. )
82 74 78 81 3eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. K , ( I ` w ) >. ( <. <. X , z >. , <. X , w >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. ( ( Id ` C ) ` X ) , f >. ) = ( <. ( ( Id ` C ) ` Y ) , f >. ( <. <. X , z >. , <. Y , z >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. K , ( I ` z ) >. ) )
83 82 fveq2d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( <. X , z >. ( 2nd ` F ) <. Y , w >. ) ` ( <. K , ( I ` w ) >. ( <. <. X , z >. , <. X , w >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. ( ( Id ` C ) ` X ) , f >. ) ) = ( ( <. X , z >. ( 2nd ` F ) <. Y , w >. ) ` ( <. ( ( Id ` C ) ` Y ) , f >. ( <. <. X , z >. , <. Y , z >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. K , ( I ` z ) >. ) ) )
84 eqid 
 |-  ( comp ` E ) = ( comp ` E )
85 21 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( 1st ` F ) ( ( C Xc. D ) Func E ) ( 2nd ` F ) )
86 24 3ad2antr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. X , z >. e. ( A X. B ) )
87 59 69 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. X , w >. e. ( A X. B ) )
88 61 69 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. Y , w >. e. ( A X. B ) )
89 76 70 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` X ) , f >. e. ( ( X H X ) X. ( z ( Hom ` D ) w ) ) )
90 15 2 6 7 28 59 67 59 69 17 xpchom2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. X , w >. ) = ( ( X H X ) X. ( z ( Hom ` D ) w ) ) )
91 89 90 eleqtrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` X ) , f >. e. ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. X , w >. ) )
92 62 77 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. K , ( I ` w ) >. e. ( ( X H Y ) X. ( w ( Hom ` D ) w ) ) )
93 15 2 6 7 28 59 69 61 69 17 xpchom2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. X , w >. ( Hom ` ( C Xc. D ) ) <. Y , w >. ) = ( ( X H Y ) X. ( w ( Hom ` D ) w ) ) )
94 92 93 eleqtrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. K , ( I ` w ) >. e. ( <. X , w >. ( Hom ` ( C Xc. D ) ) <. Y , w >. ) )
95 16 17 75 84 85 86 87 88 91 94 funcco 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( <. X , z >. ( 2nd ` F ) <. Y , w >. ) ` ( <. K , ( I ` w ) >. ( <. <. X , z >. , <. X , w >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. ( ( Id ` C ) ` X ) , f >. ) ) = ( ( ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ` <. K , ( I ` w ) >. ) ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. X , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , f >. ) ) )
96 26 3ad2antr1 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. Y , z >. e. ( A X. B ) )
97 62 79 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. K , ( I ` z ) >. e. ( ( X H Y ) X. ( z ( Hom ` D ) z ) ) )
98 15 2 6 7 28 59 67 61 67 17 xpchom2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. Y , z >. ) = ( ( X H Y ) X. ( z ( Hom ` D ) z ) ) )
99 97 98 eleqtrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. K , ( I ` z ) >. e. ( <. X , z >. ( Hom ` ( C Xc. D ) ) <. Y , z >. ) )
100 80 70 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` Y ) , f >. e. ( ( Y H Y ) X. ( z ( Hom ` D ) w ) ) )
101 15 2 6 7 28 61 67 61 69 17 xpchom2 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. Y , z >. ( Hom ` ( C Xc. D ) ) <. Y , w >. ) = ( ( Y H Y ) X. ( z ( Hom ` D ) w ) ) )
102 100 101 eleqtrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( Id ` C ) ` Y ) , f >. e. ( <. Y , z >. ( Hom ` ( C Xc. D ) ) <. Y , w >. ) )
103 16 17 75 84 85 86 96 88 99 102 funcco 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( <. X , z >. ( 2nd ` F ) <. Y , w >. ) ` ( <. ( ( Id ` C ) ` Y ) , f >. ( <. <. X , z >. , <. Y , z >. >. ( comp ` ( C Xc. D ) ) <. Y , w >. ) <. K , ( I ` z ) >. ) ) = ( ( ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) ` <. ( ( Id ` C ) ` Y ) , f >. ) ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. Y , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) ( ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ` <. K , ( I ` z ) >. ) ) )
104 83 95 103 3eqtr3d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ` <. K , ( I ` w ) >. ) ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. X , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , f >. ) ) = ( ( ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) ` <. ( ( Id ` C ) ` Y ) , f >. ) ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. Y , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) ( ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ` <. K , ( I ` z ) >. ) ) )
105 5 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> F e. ( ( C Xc. D ) Func E ) )
106 1 2 58 66 105 6 59 41 67 curf11 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) = ( X ( 1st ` F ) z ) )
107 106 43 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) = ( ( 1st ` F ) ` <. X , z >. ) )
108 1 2 58 66 105 6 59 41 69 curf11 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) = ( X ( 1st ` F ) w ) )
109 df-ov 
 |-  ( X ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. X , w >. )
110 108 109 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) = ( ( 1st ` F ) ` <. X , w >. ) )
111 107 110 opeq12d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) >. = <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. X , w >. ) >. )
112 1 2 58 66 105 6 61 45 69 curf11 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) = ( Y ( 1st ` F ) w ) )
113 df-ov 
 |-  ( Y ( 1st ` F ) w ) = ( ( 1st ` F ) ` <. Y , w >. )
114 112 113 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) = ( ( 1st ` F ) ` <. Y , w >. ) )
115 111 114 oveq12d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) = ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. X , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) )
116 1 2 58 66 105 6 7 8 59 61 62 12 69 curf2val 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( L ` w ) = ( K ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ( I ` w ) ) )
117 df-ov 
 |-  ( K ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ( I ` w ) ) = ( ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ` <. K , ( I ` w ) >. )
118 116 117 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( L ` w ) = ( ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ` <. K , ( I ` w ) >. ) )
119 1 2 58 66 105 6 59 41 67 28 57 69 70 curf12 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( z ( 2nd ` ( ( 1st ` G ) ` X ) ) w ) ` f ) = ( ( ( Id ` C ) ` X ) ( <. X , z >. ( 2nd ` F ) <. X , w >. ) f ) )
120 df-ov 
 |-  ( ( ( Id ` C ) ` X ) ( <. X , z >. ( 2nd ` F ) <. X , w >. ) f ) = ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , f >. )
121 119 120 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( z ( 2nd ` ( ( 1st ` G ) ` X ) ) w ) ` f ) = ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , f >. ) )
122 115 118 121 oveq123d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( L ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` G ) ` X ) ) w ) ` f ) ) = ( ( ( <. X , w >. ( 2nd ` F ) <. Y , w >. ) ` <. K , ( I ` w ) >. ) ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. X , w >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) ( ( <. X , z >. ( 2nd ` F ) <. X , w >. ) ` <. ( ( Id ` C ) ` X ) , f >. ) ) )
123 1 2 58 66 105 6 61 45 67 curf11 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) = ( Y ( 1st ` F ) z ) )
124 123 47 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) = ( ( 1st ` F ) ` <. Y , z >. ) )
125 107 124 opeq12d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) >. = <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. Y , z >. ) >. )
126 125 114 oveq12d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) = ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. Y , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) )
127 1 2 58 66 105 6 61 45 67 28 57 69 70 curf12 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( z ( 2nd ` ( ( 1st ` G ) ` Y ) ) w ) ` f ) = ( ( ( Id ` C ) ` Y ) ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) f ) )
128 df-ov 
 |-  ( ( ( Id ` C ) ` Y ) ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) f ) = ( ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) ` <. ( ( Id ` C ) ` Y ) , f >. )
129 127 128 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( z ( 2nd ` ( ( 1st ` G ) ` Y ) ) w ) ` f ) = ( ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) ` <. ( ( Id ` C ) ` Y ) , f >. ) )
130 1 2 58 66 105 6 7 8 59 61 62 12 67 curf2val 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( L ` z ) = ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) )
131 df-ov 
 |-  ( K ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ( I ` z ) ) = ( ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ` <. K , ( I ` z ) >. )
132 130 131 eqtrdi 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( L ` z ) = ( ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ` <. K , ( I ` z ) >. ) )
133 126 129 132 oveq123d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( ( z ( 2nd ` ( ( 1st ` G ) ` Y ) ) w ) ` f ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( L ` z ) ) = ( ( ( <. Y , z >. ( 2nd ` F ) <. Y , w >. ) ` <. ( ( Id ` C ) ` Y ) , f >. ) ( <. ( ( 1st ` F ) ` <. X , z >. ) , ( ( 1st ` F ) ` <. Y , z >. ) >. ( comp ` E ) ( ( 1st ` F ) ` <. Y , w >. ) ) ( ( <. X , z >. ( 2nd ` F ) <. Y , z >. ) ` <. K , ( I ` z ) >. ) ) )
134 104 122 133 3eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B /\ f e. ( z ( Hom ` D ) w ) ) ) -> ( ( L ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` G ) ` X ) ) w ) ` f ) ) = ( ( ( z ( 2nd ` ( ( 1st ` G ) ` Y ) ) w ) ` f ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( L ` z ) ) )
135 134 ralrimivvva 
 |-  ( ph -> A. z e. B A. w e. B A. f e. ( z ( Hom ` D ) w ) ( ( L ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` G ) ` X ) ) w ) ` f ) ) = ( ( ( z ( 2nd ` ( ( 1st ` G ) ` Y ) ) w ) ` f ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( L ` z ) ) )
136 1 2 3 4 5 6 9 41 curf1cl 
 |-  ( ph -> ( ( 1st ` G ) ` X ) e. ( D Func E ) )
137 1 2 3 4 5 6 10 45 curf1cl 
 |-  ( ph -> ( ( 1st ` G ) ` Y ) e. ( D Func E ) )
138 13 6 28 18 84 136 137 isnat2 
 |-  ( ph -> ( L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) <-> ( L e. X_ z e. B ( ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) ( Hom ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) ) /\ A. z e. B A. w e. B A. f e. ( z ( Hom ` D ) w ) ( ( L ` w ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` w ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( ( z ( 2nd ` ( ( 1st ` G ) ` X ) ) w ) ` f ) ) = ( ( ( z ( 2nd ` ( ( 1st ` G ) ` Y ) ) w ) ` f ) ( <. ( ( 1st ` ( ( 1st ` G ) ` X ) ) ` z ) , ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` z ) >. ( comp ` E ) ( ( 1st ` ( ( 1st ` G ) ` Y ) ) ` w ) ) ( L ` z ) ) ) ) )
139 56 135 138 mpbir2and 
 |-  ( ph -> L e. ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) )