hofval

Description: Value of the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from ( oppCatC ) X. C to SetCat , whose object part is the hom-function Hom , and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	$⊢ M = {Hom}_{F} (C)$
	hofval.c	$⊢ φ \to C \in Cat$
	hofval.b	$⊢ B = {Base}_{C}$
	hofval.h	$⊢ H = Hom (C)$
	hofval.o	$⊢ \underset{˙}{\cdot} = comp (C)$
Assertion	hofval	$⊢ φ \to M = ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩$

Proof

Step	Hyp	Ref	Expression
1		hofval.m	$⊢ M = {Hom}_{F} (C)$
2		hofval.c	$⊢ φ \to C \in Cat$
3		hofval.b	$⊢ B = {Base}_{C}$
4		hofval.h	$⊢ H = Hom (C)$
5		hofval.o	$⊢ \underset{˙}{\cdot} = comp (C)$
6		df-hof	$⊢ {Hom}_{F} = (c \in Cat ⟼ ⟨{Hom}_{𝑓} (c), ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (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		simpr	$⊢ (φ \land c = C) \to c = C$
8	7	fveq2d	$⊢ (φ \land c = C) \to {Hom}_{𝑓} (c) = {Hom}_{𝑓} (C)$
9		fvexd	$⊢ (φ \land c = C) \to {Base}_{c} \in V$
10	7	fveq2d	$⊢ (φ \land c = C) \to {Base}_{c} = {Base}_{C}$
11	10 3	eqtr4di	$⊢ (φ \land c = C) \to {Base}_{c} = B$
12		simpr	$⊢ ((φ \land c = C) \land b = B) \to b = B$
13	12	sqxpeqd	$⊢ ((φ \land c = C) \land b = B) \to b \times b = B \times B$
14		simplr	$⊢ ((φ \land c = C) \land b = B) \to c = C$
15	14	fveq2d	$⊢ ((φ \land c = C) \land b = B) \to Hom (c) = Hom (C)$
16	15 4	eqtr4di	$⊢ ((φ \land c = C) \land b = B) \to Hom (c) = H$
17	16	oveqd	$⊢ ((φ \land c = C) \land b = B) \to 1^{st} (y) Hom (c) 1^{st} (x) = 1^{st} (y) H 1^{st} (x)$
18	16	oveqd	$⊢ ((φ \land c = C) \land b = B) \to 2^{nd} (x) Hom (c) 2^{nd} (y) = 2^{nd} (x) H 2^{nd} (y)$
19	16	fveq1d	$⊢ ((φ \land c = C) \land b = B) \to Hom (c) (x) = H (x)$
20	14	fveq2d	$⊢ ((φ \land c = C) \land b = B) \to comp (c) = comp (C)$
21	20 5	eqtr4di	$⊢ ((φ \land c = C) \land b = B) \to comp (c) = \underset{˙}{\cdot}$
22	21	oveqd	$⊢ ((φ \land c = C) \land b = B) \to ⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y) = ⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)$
23	21	oveqd	$⊢ ((φ \land c = C) \land b = B) \to x comp (c) 2^{nd} (y) = x \underset{˙}{\cdot} 2^{nd} (y)$
24	23	oveqd	$⊢ ((φ \land c = C) \land b = B) \to g (x comp (c) 2^{nd} (y)) h = g (x \underset{˙}{\cdot} 2^{nd} (y)) h$
25		eqidd	$⊢ ((φ \land c = C) \land b = B) \to f = f$
26	22 24 25	oveq123d	$⊢ ((φ \land c = C) \land b = B) \to (g (x comp (c) 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ comp (c) 2^{nd} (y)) f = (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f$
27	19 26	mpteq12dv	$⊢ ((φ \land c = C) \land b = B) \to (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) = (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)$
28	17 18 27	mpoeq123dv	$⊢ ((φ \land c = C) \land b = B) \to (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)) = (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f))$
29	13 13 28	mpoeq123dv	$⊢ ((φ \land c = C) \land b = B) \to (x \in (b \times b), y \in (b \times b) ⟼ (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))) = (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))$
30	9 11 29	csbied2	$⊢ (φ \land c = C) \to ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (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))) = (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))$
31	8 30	opeq12d	$⊢ (φ \land c = C) \to ⟨{Hom}_{𝑓} (c), ⦋ {Base}_{c} / b ⦌ (x \in (b \times b), y \in (b \times b) ⟼ (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)))⟩ = ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩$
32		opex	$⊢ ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩ \in V$
33	32	a1i	$⊢ φ \to ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩ \in V$
34	6 31 2 33	fvmptd2	$⊢ φ \to {Hom}_{F} (C) = ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩$
35	1 34	syl5eq	$⊢ φ \to M = ⟨{Hom}_{𝑓} (C), (x \in (B \times B), y \in (B \times B) ⟼ (f \in (1^{st} (y) H 1^{st} (x)), g \in (2^{nd} (x) H 2^{nd} (y)) ⟼ (h \in H (x) ⟼ (g (x \underset{˙}{\cdot} 2^{nd} (y)) h) (⟨1^{st} (y), 1^{st} (x)⟩ \underset{˙}{\cdot} 2^{nd} (y)) f)))⟩$

Metamath Proof Explorer

Theorem hofval

Proof