hof2val

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	$⊢ φ \to C \in Cat$
	hof1.b	$⊢ B = {Base}_{C}$
	hof1.h	$⊢ H = Hom (C)$
	hof1.x	$⊢ φ \to X \in B$
	hof1.y	$⊢ φ \to Y \in B$
	hof2.z	$⊢ φ \to Z \in B$
	hof2.w	$⊢ φ \to W \in B$
	hof2.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	hof2.f	$⊢ φ \to F \in (Z H X)$
	hof2.g	$⊢ φ \to G \in (Y H W)$
Assertion	hof2val	$⊢ φ \to F (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) G = (h \in (X H Y) ⟼ (G (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) F)$

Proof

Step	Hyp	Ref	Expression
1		hofval.m	$⊢ M = {Hom}_{F} (C)$
2		hofval.c	$⊢ φ \to C \in Cat$
3		hof1.b	$⊢ B = {Base}_{C}$
4		hof1.h	$⊢ H = Hom (C)$
5		hof1.x	$⊢ φ \to X \in B$
6		hof1.y	$⊢ φ \to Y \in B$
7		hof2.z	$⊢ φ \to Z \in B$
8		hof2.w	$⊢ φ \to W \in B$
9		hof2.o	$⊢ \underset{˙}{\cdot} = comp (C)$
10		hof2.f	$⊢ φ \to F \in (Z H X)$
11		hof2.g	$⊢ φ \to G \in (Y H W)$
12	1 2 3 4 5 6 7 8 9	hof2fval	$⊢ φ \to ⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩ = (f \in (Z H X), g \in (Y H W) ⟼ (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f))$
13		simplrr	$⊢ ((φ \land (f = F \land g = G)) \land h \in (X H Y)) \to g = G$
14	13	oveq1d	$⊢ ((φ \land (f = F \land g = G)) \land h \in (X H Y)) \to g (⟨X, Y⟩ \underset{˙}{\cdot} W) h = G (⟨X, Y⟩ \underset{˙}{\cdot} W) h$
15		simplrl	$⊢ ((φ \land (f = F \land g = G)) \land h \in (X H Y)) \to f = F$
16	14 15	oveq12d	$⊢ ((φ \land (f = F \land g = G)) \land h \in (X H Y)) \to (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f = (G (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) F$
17	16	mpteq2dva	$⊢ (φ \land (f = F \land g = G)) \to (h \in (X H Y) ⟼ (g (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) f) = (h \in (X H Y) ⟼ (G (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) F)$
18		ovex	$⊢ X H Y \in V$
19	18	mptex	$⊢ (h \in (X H Y) ⟼ (G (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) F) \in V$
20	19	a1i	$⊢ φ \to (h \in (X H Y) ⟼ (G (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) F) \in V$
21	12 17 10 11 20	ovmpod	$⊢ φ \to F (⟨X, Y⟩ 2^{nd} (M) ⟨Z, W⟩) G = (h \in (X H Y) ⟼ (G (⟨X, Y⟩ \underset{˙}{\cdot} W) h) (⟨Z, X⟩ \underset{˙}{\cdot} W) F)$

Metamath Proof Explorer

Theorem hof2val

Proof