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

Metamath Proof Explorer

Theorem curf1fval

Description: Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses curfval.g ⊢ G = C D curry F F
curfval.a ⊢ A = Base C
curfval.c ⊢ φ → C ∈ Cat
curfval.d ⊢ φ → D ∈ Cat
curfval.f ⊢ φ → F ∈ C × c D Func E
curfval.b ⊢ B = Base D
curfval.j ⊢ J = Hom ⁡ D
curfval.1 ⊢ 1 ˙ = Id ⁡ C
Assertion curf1fval ⊢ φ → 1 st ⁡ G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y J z ⟼ 1 ˙ ⁡ x x y 2 nd ⁡ F x z g

Proof

Step Hyp Ref Expression
1 curfval.g ⊢ G = C D curry F F
2 curfval.a ⊢ A = Base C
3 curfval.c ⊢ φ → C ∈ Cat
4 curfval.d ⊢ φ → D ∈ Cat
5 curfval.f ⊢ φ → F ∈ C × c D Func E
6 curfval.b ⊢ B = Base D
7 curfval.j ⊢ J = Hom ⁡ D
8 curfval.1 ⊢ 1 ˙ = Id ⁡ C
9 eqid ⊢ Hom ⁡ C = Hom ⁡ C
10 eqid ⊢ Id ⁡ D = Id ⁡ D
11 1 2 3 4 5 6 7 8 9 10 curfval ⊢ φ → G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y J z ⟼ 1 ˙ ⁡ x x y 2 nd ⁡ F x z g x ∈ A , y ∈ A ⟼ g ∈ x Hom ⁡ C y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z Id ⁡ D ⁡ z
12 2 fvexi ⊢ A ∈ V
13 12 mptex ⊢ x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y J z ⟼ 1 ˙ ⁡ x x y 2 nd ⁡ F x z g ∈ V
14 12 12 mpoex ⊢ x ∈ A , y ∈ A ⟼ g ∈ x Hom ⁡ C y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z Id ⁡ D ⁡ z ∈ V
15 13 14 op1std ⊢ G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y J z ⟼ 1 ˙ ⁡ x x y 2 nd ⁡ F x z g x ∈ A , y ∈ A ⟼ g ∈ x Hom ⁡ C y ⟼ z ∈ B ⟼ g x z 2 nd ⁡ F y z Id ⁡ D ⁡ z → 1 st ⁡ G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y J z ⟼ 1 ˙ ⁡ x x y 2 nd ⁡ F x z g
16 11 15 syl ⊢ φ → 1 st ⁡ G = x ∈ A ⟼ y ∈ B ⟼ x 1 st ⁡ F y y ∈ B , z ∈ B ⟼ g ∈ y J z ⟼ 1 ˙ ⁡ x x y 2 nd ⁡ F x z g