Metamath Proof Explorer

Theorem curf2

Description: Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017)

Ref Expression
Hypotheses curf2.g ⊢ G = C D curry F F
curf2.a ⊢ A = Base C
curf2.c ⊢ φ → C ∈ Cat
curf2.d ⊢ φ → D ∈ Cat
curf2.f ⊢ φ → F ∈ C × c D Func E
curf2.b ⊢ B = Base D
curf2.h ⊢ H = Hom ⁡ C
curf2.i ⊢ I = Id ⁡ D
curf2.x ⊢ φ → X ∈ A
curf2.y ⊢ φ → Y ∈ A
curf2.k ⊢ φ → K ∈ X H Y
curf2.l ⊢ L = X 2 nd ⁡ G Y ⁡ K
Assertion curf2 ⊢ φ → L = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z

Proof

Step Hyp Ref Expression
1 curf2.g ⊢ G = C D curry F F
2 curf2.a ⊢ A = Base C
3 curf2.c ⊢ φ → C ∈ Cat
4 curf2.d ⊢ φ → D ∈ Cat
5 curf2.f ⊢ φ → F ∈ C × c D Func E
6 curf2.b ⊢ B = Base D
7 curf2.h ⊢ H = Hom ⁡ C
8 curf2.i ⊢ I = Id ⁡ D
9 curf2.x ⊢ φ → X ∈ A
10 curf2.y ⊢ φ → Y ∈ A
11 curf2.k ⊢ φ → K ∈ X H Y
12 curf2.l ⊢ L = X 2 nd ⁡ G Y ⁡ K
13 eqid ⊢ Hom ⁡ D = Hom ⁡ D
14 eqid ⊢ Id ⁡ C = Id ⁡ C
15 1 2 3 4 5 6 13 14 7 8 curfval ⊢ φ → G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y Hom ⁡ D z ⟼ Id ⁡ C ⁡ x x y 2 nd ⁡ F x z g x ∈ A , y ∈ A ⟼ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z
16 2 fvexi ⊢ A ∈ V
17 16 mptex ⊢ x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y Hom ⁡ D z ⟼ Id ⁡ C ⁡ x x y 2 nd ⁡ F x z g ∈ V
18 16 16 mpoex ⊢ x ∈ A , y ∈ A ⟼ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z ∈ V
19 17 18 op2ndd ⊢ G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y Hom ⁡ D z ⟼ Id ⁡ C ⁡ x x y 2 nd ⁡ F x z g x ∈ A , y ∈ A ⟼ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z → 2 nd ⁡ G = x ∈ A , y ∈ A ⟼ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z
20 15 19 syl ⊢ φ → 2 nd ⁡ G = x ∈ A , y ∈ A ⟼ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z
21 10 adantr ⊢ φ ∧ x = X → Y ∈ A
22 ovex ⊢ x H y ∈ V
23 22 mptex ⊢ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z ∈ V
24 23 a1i ⊢ φ ∧ x = X ∧ y = Y → g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z ∈ V
25 11 adantr ⊢ φ ∧ x = X ∧ y = Y → K ∈ X H Y
26 simprl ⊢ φ ∧ x = X ∧ y = Y → x = X
27 simprr ⊢ φ ∧ x = X ∧ y = Y → y = Y
28 26 27 oveq12d ⊢ φ ∧ x = X ∧ y = Y → x H y = X H Y
29 25 28 eleqtrrd ⊢ φ ∧ x = X ∧ y = Y → K ∈ x H y
30 6 fvexi ⊢ B ∈ V
31 30 mptex ⊢ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z ∈ V
32 31 a1i ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z ∈ V
33 simplrl ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → x = X
34 33 opeq1d ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → x z = X z
35 simplrr ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → y = Y
36 35 opeq1d ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → y z = Y z
37 34 36 oveq12d ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → x z 2 nd ⁡ F y z = X z 2 nd ⁡ F Y z
38 simpr ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → g = K
39 eqidd ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → I ⁡ z = I ⁡ z
40 37 38 39 oveq123d ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → g x z 2 nd ⁡ F y z I ⁡ z = K X z 2 nd ⁡ F Y z I ⁡ z
41 40 mpteq2dv ⊢ φ ∧ x = X ∧ y = Y ∧ g = K → z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z
42 29 32 41 fvmptdv2 ⊢ φ ∧ x = X ∧ y = Y → X 2 nd ⁡ G Y = g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z → X 2 nd ⁡ G Y ⁡ K = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z
43 9 21 24 42 ovmpodv ⊢ φ → 2 nd ⁡ G = x ∈ A , y ∈ A ⟼ g ∈ x H y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z I ⁡ z → X 2 nd ⁡ G Y ⁡ K = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z
44 20 43 mpd ⊢ φ → X 2 nd ⁡ G Y ⁡ K = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z
45 12 44 eqtrid ⊢ φ → L = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z