hof1fval

Description: The object part of the Hom functor is the Homf operation, which is just a functionalized version of Hom . That is, it is a two argument function, which maps X , Y to the set of morphisms from X to Y . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	$⊢ M = {Hom}_{F} (C)$
	hofval.c	$⊢ φ \to C \in Cat$
Assertion	hof1fval	$⊢ φ \to 1^{st} (M) = {Hom}_{𝑓} (C)$

Proof

Step	Hyp	Ref	Expression
1		hofval.m	$⊢ M = {Hom}_{F} (C)$
2		hofval.c	$⊢ φ \to C \in Cat$
3		eqid	$⊢ {Base}_{C} = {Base}_{C}$
4		eqid	$⊢ Hom (C) = Hom (C)$
5		eqid	$⊢ comp (C) = comp (C)$
6	1 2 3 4 5	hofval	$⊢ φ \to M = ⟨{Hom}_{𝑓} (C), (x \in ({Base}_{C} \times {Base}_{C}), y \in ({Base}_{C} \times {Base}_{C}) ⟼ (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f)))⟩$
7		fvex	$⊢ {Hom}_{𝑓} (C) \in V$
8		fvex	$⊢ {Base}_{C} \in V$
9	8 8	xpex	$⊢ {Base}_{C} \times {Base}_{C} \in V$
10	9 9	mpoex	$⊢ (x \in ({Base}_{C} \times {Base}_{C}), y \in ({Base}_{C} \times {Base}_{C}) ⟼ (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f))) \in V$
11	7 10	op1std	$⊢ M = ⟨{Hom}_{𝑓} (C), (x \in ({Base}_{C} \times {Base}_{C}), y \in ({Base}_{C} \times {Base}_{C}) ⟼ (f \in (1^{st} (y) Hom (C) 1^{st} (x)), g \in (2^{nd} (x) Hom (C) 2^{nd} (y)) ⟼ (h \in Hom (C) (x) ⟼ (g (x comp (C) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (C) 2^{nd} (y)) f)))⟩ \to 1^{st} (M) = {Hom}_{𝑓} (C)$
12	6 11	syl	$⊢ φ \to 1^{st} (M) = {Hom}_{𝑓} (C)$

Metamath Proof Explorer

Theorem hof1fval

Proof