homaval

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		homaval.j	$⊢ J = Hom (C)$
5		homaval.x	$⊢ φ \to X \in B$
6		homaval.y	$⊢ φ \to Y \in B$
7		df-ov	$⊢ X H Y = H (⟨X, Y⟩)$
8	1 2 3 4	homafval	$⊢ φ \to H = (z \in (B \times B) ⟼ \{z\} \times J (z))$
9		simpr	$⊢ (φ \land z = ⟨X, Y⟩) \to z = ⟨X, Y⟩$
10	9	sneqd	$⊢ (φ \land z = ⟨X, Y⟩) \to \{z\} = \{⟨X, Y⟩\}$
11	9	fveq2d	$⊢ (φ \land z = ⟨X, Y⟩) \to J (z) = J (⟨X, Y⟩)$
12		df-ov	$⊢ X J Y = J (⟨X, Y⟩)$
13	11 12	eqtr4di	$⊢ (φ \land z = ⟨X, Y⟩) \to J (z) = X J Y$
14	10 13	xpeq12d	$⊢ (φ \land z = ⟨X, Y⟩) \to \{z\} \times J (z) = \{⟨X, Y⟩\} \times (X J Y)$
15	5 6	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (B \times B)$
16		snex	$⊢ \{⟨X, Y⟩\} \in V$
17		ovex	$⊢ X J Y \in V$
18	16 17	xpex	$⊢ \{⟨X, Y⟩\} \times (X J Y) \in V$
19	18	a1i	$⊢ φ \to \{⟨X, Y⟩\} \times (X J Y) \in V$
20	8 14 15 19	fvmptd	$⊢ φ \to H (⟨X, Y⟩) = \{⟨X, Y⟩\} \times (X J Y)$
21	7 20	eqtrid	$⊢ φ \to X H Y = \{⟨X, Y⟩\} \times (X J Y)$

Metamath Proof Explorer