Metamath Proof Explorer

Theorem hof2

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses hofval.m ⊢ M = Hom F ⁡ C
hofval.c ⊢ φ → C ∈ Cat
hof1.b ⊢ B = Base C
hof1.h ⊢ H = Hom ⁡ C
hof1.x ⊢ φ → X ∈ B
hof1.y ⊢ φ → Y ∈ B
hof2.z ⊢ φ → Z ∈ B
hof2.w ⊢ φ → W ∈ B
hof2.o ⊢ · ˙ = comp ⁡ C
hof2.f ⊢ φ → F ∈ Z H X
hof2.g ⊢ φ → G ∈ Y H W
hof2.k ⊢ φ → K ∈ X H Y
Assertion hof2 ⊢ φ → F X Y 2 nd ⁡ M Z W G ⁡ K = G X Y · ˙ W K Z X · ˙ W F

Proof

Step Hyp Ref Expression
1 hofval.m ⊢ M = Hom F ⁡ C
2 hofval.c ⊢ φ → C ∈ Cat
3 hof1.b ⊢ B = Base C
4 hof1.h ⊢ H = Hom ⁡ C
5 hof1.x ⊢ φ → X ∈ B
6 hof1.y ⊢ φ → Y ∈ B
7 hof2.z ⊢ φ → Z ∈ B
8 hof2.w ⊢ φ → W ∈ B
9 hof2.o ⊢ · ˙ = comp ⁡ C
10 hof2.f ⊢ φ → F ∈ Z H X
11 hof2.g ⊢ φ → G ∈ Y H W
12 hof2.k ⊢ φ → K ∈ X H Y
13 1 2 3 4 5 6 7 8 9 10 11 hof2val ⊢ φ → F X Y 2 nd ⁡ M Z W G = h ∈ X H Y ⟼ G X Y · ˙ W h Z X · ˙ W F
14 simpr ⊢ φ ∧ h = K → h = K
15 14 oveq2d ⊢ φ ∧ h = K → G X Y · ˙ W h = G X Y · ˙ W K
16 15 oveq1d ⊢ φ ∧ h = K → G X Y · ˙ W h Z X · ˙ W F = G X Y · ˙ W K Z X · ˙ W F
17 ovexd ⊢ φ → G X Y · ˙ W K Z X · ˙ W F ∈ V
18 13 16 12 17 fvmptd ⊢ φ → F X Y 2 nd ⁡ M Z W G ⁡ K = G X Y · ˙ W K Z X · ˙ W F