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

Metamath Proof Explorer

Theorem curf2val

Description: Value of a component of the curry functor natural transformation. (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
curf2.z ⊢ φ → Z ∈ B
Assertion curf2val ⊢ φ → L ⁡ Z = 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 curf2.z ⊢ φ → Z ∈ B
14 1 2 3 4 5 6 7 8 9 10 11 12 curf2 ⊢ φ → L = z ∈ B ⟼ K X z 2 nd ⁡ F Y z I ⁡ z
15 simpr ⊢ φ ∧ z = Z → z = Z
16 15 opeq2d ⊢ φ ∧ z = Z → X z = X Z
17 15 opeq2d ⊢ φ ∧ z = Z → Y z = Y Z
18 16 17 oveq12d ⊢ φ ∧ z = Z → X z 2 nd ⁡ F Y z = X Z 2 nd ⁡ F Y Z
19 eqidd ⊢ φ ∧ z = Z → K = K
20 15 fveq2d ⊢ φ ∧ z = Z → I ⁡ z = I ⁡ Z
21 18 19 20 oveq123d ⊢ φ ∧ z = Z → K X z 2 nd ⁡ F Y z I ⁡ z = K X Z 2 nd ⁡ F Y Z I ⁡ Z
22 ovexd ⊢ φ → K X Z 2 nd ⁡ F Y Z I ⁡ Z ∈ V
23 14 21 13 22 fvmptd ⊢ φ → L ⁡ Z = K X Z 2 nd ⁡ F Y Z I ⁡ Z