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=CDcurryFF
curf2.a A=BaseC
curf2.c φCCat
curf2.d φDCat
curf2.f φFC×cDFuncE
curf2.b B=BaseD
curf2.h H=HomC
curf2.i I=IdD
curf2.x φXA
curf2.y φYA
curf2.k φKXHY
curf2.l L=X2ndGYK
curf2.n N=DNatE
Assertion curf2cl φL1stGXN1stGY

Proof

Step Hyp Ref Expression
1 curf2.g G=CDcurryFF
2 curf2.a A=BaseC
3 curf2.c φCCat
4 curf2.d φDCat
5 curf2.f φFC×cDFuncE
6 curf2.b B=BaseD
7 curf2.h H=HomC
8 curf2.i I=IdD
9 curf2.x φXA
10 curf2.y φYA
11 curf2.k φKXHY
12 curf2.l L=X2ndGYK
13 curf2.n N=DNatE
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 φL=zBKXz2ndFYzIz
15 eqid C×cD=C×cD
16 15 2 6 xpcbas A×B=BaseC×cD
17 eqid HomC×cD=HomC×cD
18 eqid HomE=HomE
19 relfunc RelC×cDFuncE
20 1st2ndbr RelC×cDFuncEFC×cDFuncE1stFC×cDFuncE2ndF
21 19 5 20 sylancr φ1stFC×cDFuncE2ndF
22 21 adantr φzB1stFC×cDFuncE2ndF
23 opelxpi XAzBXzA×B
24 9 23 sylan φzBXzA×B
25 opelxpi YAzBYzA×B
26 10 25 sylan φzBYzA×B
27 16 17 18 22 24 26 funcf2 φzBXz2ndFYz:XzHomC×cDYz1stFXzHomE1stFYz
28 eqid HomD=HomD
29 9 adantr φzBXA
30 simpr φzBzB
31 10 adantr φzBYA
32 15 2 6 7 28 29 30 31 30 17 xpchom2 φzBXzHomC×cDYz=XHY×zHomDz
33 32 feq2d φzBXz2ndFYz:XzHomC×cDYz1stFXzHomE1stFYzXz2ndFYz:XHY×zHomDz1stFXzHomE1stFYz
34 27 33 mpbid φzBXz2ndFYz:XHY×zHomDz1stFXzHomE1stFYz
35 11 adantr φzBKXHY
36 4 adantr φzBDCat
37 6 28 8 36 30 catidcl φzBIzzHomDz
38 34 35 37 fovrnd φzBKXz2ndFYzIz1stFXzHomE1stFYz
39 3 adantr φzBCCat
40 5 adantr φzBFC×cDFuncE
41 eqid 1stGX=1stGX
42 1 2 39 36 40 6 29 41 30 curf11 φzB1st1stGXz=X1stFz
43 df-ov X1stFz=1stFXz
44 42 43 eqtrdi φzB1st1stGXz=1stFXz
45 eqid 1stGY=1stGY
46 1 2 39 36 40 6 31 45 30 curf11 φzB1st1stGYz=Y1stFz
47 df-ov Y1stFz=1stFYz
48 46 47 eqtrdi φzB1st1stGYz=1stFYz
49 44 48 oveq12d φzB1st1stGXzHomE1st1stGYz=1stFXzHomE1stFYz
50 38 49 eleqtrrd φzBKXz2ndFYzIz1st1stGXzHomE1st1stGYz
51 50 ralrimiva φzBKXz2ndFYzIz1st1stGXzHomE1st1stGYz
52 6 fvexi BV
53 mptelixpg BVzBKXz2ndFYzIzzB1st1stGXzHomE1st1stGYzzBKXz2ndFYzIz1st1stGXzHomE1st1stGYz
54 52 53 ax-mp zBKXz2ndFYzIzzB1st1stGXzHomE1st1stGYzzBKXz2ndFYzIz1st1stGXzHomE1st1stGYz
55 51 54 sylibr φzBKXz2ndFYzIzzB1st1stGXzHomE1st1stGYz
56 14 55 eqeltrd φLzB1st1stGXzHomE1st1stGYz
57 eqid IdC=IdC
58 3 adantr φzBwBfzHomDwCCat
59 9 adantr φzBwBfzHomDwXA
60 eqid compC=compC
61 10 adantr φzBwBfzHomDwYA
62 11 adantr φzBwBfzHomDwKXHY
63 2 7 57 58 59 60 61 62 catrid φzBwBfzHomDwKXXcompCYIdCX=K
64 2 7 57 58 59 60 61 62 catlid φzBwBfzHomDwIdCYXYcompCYK=K
65 63 64 eqtr4d φzBwBfzHomDwKXXcompCYIdCX=IdCYXYcompCYK
66 4 adantr φzBwBfzHomDwDCat
67 simpr1 φzBwBfzHomDwzB
68 eqid compD=compD
69 simpr2 φzBwBfzHomDwwB
70 simpr3 φzBwBfzHomDwfzHomDw
71 6 28 8 66 67 68 69 70 catlid φzBwBfzHomDwIwzwcompDwf=f
72 6 28 8 66 67 68 69 70 catrid φzBwBfzHomDwfzzcompDwIz=f
73 71 72 eqtr4d φzBwBfzHomDwIwzwcompDwf=fzzcompDwIz
74 65 73 opeq12d φzBwBfzHomDwKXXcompCYIdCXIwzwcompDwf=IdCYXYcompCYKfzzcompDwIz
75 eqid compC×cD=compC×cD
76 2 7 57 58 59 catidcl φzBwBfzHomDwIdCXXHX
77 6 28 8 66 69 catidcl φzBwBfzHomDwIwwHomDw
78 15 2 6 7 28 59 67 59 69 60 68 75 61 69 76 70 62 77 xpcco2 φzBwBfzHomDwKIwXzXwcompC×cDYwIdCXf=KXXcompCYIdCXIwzwcompDwf
79 37 3ad2antr1 φzBwBfzHomDwIzzHomDz
80 2 7 57 58 61 catidcl φzBwBfzHomDwIdCYYHY
81 15 2 6 7 28 59 67 61 67 60 68 75 61 69 62 79 80 70 xpcco2 φzBwBfzHomDwIdCYfXzYzcompC×cDYwKIz=IdCYXYcompCYKfzzcompDwIz
82 74 78 81 3eqtr4d φzBwBfzHomDwKIwXzXwcompC×cDYwIdCXf=IdCYfXzYzcompC×cDYwKIz
83 82 fveq2d φzBwBfzHomDwXz2ndFYwKIwXzXwcompC×cDYwIdCXf=Xz2ndFYwIdCYfXzYzcompC×cDYwKIz
84 eqid compE=compE
85 21 adantr φzBwBfzHomDw1stFC×cDFuncE2ndF
86 24 3ad2antr1 φzBwBfzHomDwXzA×B
87 59 69 opelxpd φzBwBfzHomDwXwA×B
88 61 69 opelxpd φzBwBfzHomDwYwA×B
89 76 70 opelxpd φzBwBfzHomDwIdCXfXHX×zHomDw
90 15 2 6 7 28 59 67 59 69 17 xpchom2 φzBwBfzHomDwXzHomC×cDXw=XHX×zHomDw
91 89 90 eleqtrrd φzBwBfzHomDwIdCXfXzHomC×cDXw
92 62 77 opelxpd φzBwBfzHomDwKIwXHY×wHomDw
93 15 2 6 7 28 59 69 61 69 17 xpchom2 φzBwBfzHomDwXwHomC×cDYw=XHY×wHomDw
94 92 93 eleqtrrd φzBwBfzHomDwKIwXwHomC×cDYw
95 16 17 75 84 85 86 87 88 91 94 funcco φzBwBfzHomDwXz2ndFYwKIwXzXwcompC×cDYwIdCXf=Xw2ndFYwKIw1stFXz1stFXwcompE1stFYwXz2ndFXwIdCXf
96 26 3ad2antr1 φzBwBfzHomDwYzA×B
97 62 79 opelxpd φzBwBfzHomDwKIzXHY×zHomDz
98 15 2 6 7 28 59 67 61 67 17 xpchom2 φzBwBfzHomDwXzHomC×cDYz=XHY×zHomDz
99 97 98 eleqtrrd φzBwBfzHomDwKIzXzHomC×cDYz
100 80 70 opelxpd φzBwBfzHomDwIdCYfYHY×zHomDw
101 15 2 6 7 28 61 67 61 69 17 xpchom2 φzBwBfzHomDwYzHomC×cDYw=YHY×zHomDw
102 100 101 eleqtrrd φzBwBfzHomDwIdCYfYzHomC×cDYw
103 16 17 75 84 85 86 96 88 99 102 funcco φzBwBfzHomDwXz2ndFYwIdCYfXzYzcompC×cDYwKIz=Yz2ndFYwIdCYf1stFXz1stFYzcompE1stFYwXz2ndFYzKIz
104 83 95 103 3eqtr3d φzBwBfzHomDwXw2ndFYwKIw1stFXz1stFXwcompE1stFYwXz2ndFXwIdCXf=Yz2ndFYwIdCYf1stFXz1stFYzcompE1stFYwXz2ndFYzKIz
105 5 adantr φzBwBfzHomDwFC×cDFuncE
106 1 2 58 66 105 6 59 41 67 curf11 φzBwBfzHomDw1st1stGXz=X1stFz
107 106 43 eqtrdi φzBwBfzHomDw1st1stGXz=1stFXz
108 1 2 58 66 105 6 59 41 69 curf11 φzBwBfzHomDw1st1stGXw=X1stFw
109 df-ov X1stFw=1stFXw
110 108 109 eqtrdi φzBwBfzHomDw1st1stGXw=1stFXw
111 107 110 opeq12d φzBwBfzHomDw1st1stGXz1st1stGXw=1stFXz1stFXw
112 1 2 58 66 105 6 61 45 69 curf11 φzBwBfzHomDw1st1stGYw=Y1stFw
113 df-ov Y1stFw=1stFYw
114 112 113 eqtrdi φzBwBfzHomDw1st1stGYw=1stFYw
115 111 114 oveq12d φzBwBfzHomDw1st1stGXz1st1stGXwcompE1st1stGYw=1stFXz1stFXwcompE1stFYw
116 1 2 58 66 105 6 7 8 59 61 62 12 69 curf2val φzBwBfzHomDwLw=KXw2ndFYwIw
117 df-ov KXw2ndFYwIw=Xw2ndFYwKIw
118 116 117 eqtrdi φzBwBfzHomDwLw=Xw2ndFYwKIw
119 1 2 58 66 105 6 59 41 67 28 57 69 70 curf12 φzBwBfzHomDwz2nd1stGXwf=IdCXXz2ndFXwf
120 df-ov IdCXXz2ndFXwf=Xz2ndFXwIdCXf
121 119 120 eqtrdi φzBwBfzHomDwz2nd1stGXwf=Xz2ndFXwIdCXf
122 115 118 121 oveq123d φzBwBfzHomDwLw1st1stGXz1st1stGXwcompE1st1stGYwz2nd1stGXwf=Xw2ndFYwKIw1stFXz1stFXwcompE1stFYwXz2ndFXwIdCXf
123 1 2 58 66 105 6 61 45 67 curf11 φzBwBfzHomDw1st1stGYz=Y1stFz
124 123 47 eqtrdi φzBwBfzHomDw1st1stGYz=1stFYz
125 107 124 opeq12d φzBwBfzHomDw1st1stGXz1st1stGYz=1stFXz1stFYz
126 125 114 oveq12d φzBwBfzHomDw1st1stGXz1st1stGYzcompE1st1stGYw=1stFXz1stFYzcompE1stFYw
127 1 2 58 66 105 6 61 45 67 28 57 69 70 curf12 φzBwBfzHomDwz2nd1stGYwf=IdCYYz2ndFYwf
128 df-ov IdCYYz2ndFYwf=Yz2ndFYwIdCYf
129 127 128 eqtrdi φzBwBfzHomDwz2nd1stGYwf=Yz2ndFYwIdCYf
130 1 2 58 66 105 6 7 8 59 61 62 12 67 curf2val φzBwBfzHomDwLz=KXz2ndFYzIz
131 df-ov KXz2ndFYzIz=Xz2ndFYzKIz
132 130 131 eqtrdi φzBwBfzHomDwLz=Xz2ndFYzKIz
133 126 129 132 oveq123d φzBwBfzHomDwz2nd1stGYwf1st1stGXz1st1stGYzcompE1st1stGYwLz=Yz2ndFYwIdCYf1stFXz1stFYzcompE1stFYwXz2ndFYzKIz
134 104 122 133 3eqtr4d φzBwBfzHomDwLw1st1stGXz1st1stGXwcompE1st1stGYwz2nd1stGXwf=z2nd1stGYwf1st1stGXz1st1stGYzcompE1st1stGYwLz
135 134 ralrimivvva φzBwBfzHomDwLw1st1stGXz1st1stGXwcompE1st1stGYwz2nd1stGXwf=z2nd1stGYwf1st1stGXz1st1stGYzcompE1st1stGYwLz
136 1 2 3 4 5 6 9 41 curf1cl φ1stGXDFuncE
137 1 2 3 4 5 6 10 45 curf1cl φ1stGYDFuncE
138 13 6 28 18 84 136 137 isnat2 φL1stGXN1stGYLzB1st1stGXzHomE1st1stGYzzBwBfzHomDwLw1st1stGXz1st1stGXwcompE1st1stGYwz2nd1stGXwf=z2nd1stGYwf1st1stGXz1st1stGYzcompE1st1stGYwLz
139 56 135 138 mpbir2and φL1stGXN1stGY