homafval

Description: Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017)

Step	Hyp	Ref	Expression
1		homarcl.h	$⊢ H = {Hom}_{a} (C)$
2		homafval.b	$⊢ B = {Base}_{C}$
3		homafval.c	$⊢ φ \to C \in Cat$
4		homafval.j	$⊢ J = Hom (C)$
5		fveq2	$⊢ c = C \to {Base}_{c} = {Base}_{C}$
6	5 2	eqtr4di	$⊢ c = C \to {Base}_{c} = B$
7	6	sqxpeqd	$⊢ c = C \to {Base}_{c} \times {Base}_{c} = B \times B$
8		fveq2	$⊢ c = C \to Hom (c) = Hom (C)$
9	8 4	eqtr4di	$⊢ c = C \to Hom (c) = J$
10	9	fveq1d	$⊢ c = C \to Hom (c) (x) = J (x)$
11	10	xpeq2d	$⊢ c = C \to \{x\} \times Hom (c) (x) = \{x\} \times J (x)$
12	7 11	mpteq12dv	$⊢ c = C \to (x \in ({Base}_{c} \times {Base}_{c}) ⟼ \{x\} \times Hom (c) (x)) = (x \in (B \times B) ⟼ \{x\} \times J (x))$
13		df-homa	$⊢ {Hom}_{a} = (c \in Cat ⟼ (x \in ({Base}_{c} \times {Base}_{c}) ⟼ \{x\} \times Hom (c) (x)))$
14	2	fvexi	$⊢ B \in V$
15	14 14	xpex	$⊢ B \times B \in V$
16	15	mptex	$⊢ (x \in (B \times B) ⟼ \{x\} \times J (x)) \in V$
17	12 13 16	fvmpt	$⊢ C \in Cat \to {Hom}_{a} (C) = (x \in (B \times B) ⟼ \{x\} \times J (x))$
18	3 17	syl	$⊢ φ \to {Hom}_{a} (C) = (x \in (B \times B) ⟼ \{x\} \times J (x))$
19	1 18	syl5eq	$⊢ φ \to H = (x \in (B \times B) ⟼ \{x\} \times J (x))$

Metamath Proof Explorer