Theorem homaval

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

	Ref	Expression
Hypotheses	homarcl.h	$$⊢H={Hom}_a\left(C\right)$$
	homafval.b	$$⊢B={\mathrm{Base}}_C$$
	homafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	homaval.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
	homaval.x	$$⊢\phi \to X\in B$$
	homaval.y	$$⊢\phi \to Y\in B$$
Assertion	homaval	$$⊢\phi \to XHY=\left\{⟨X,Y⟩\right\}\times \left(XJY\right)$$

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	$$⊢H={Hom}_a\left(C\right)$$
2		homafval.b	$$⊢B={\mathrm{Base}}_C$$
3		homafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		homaval.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
5		homaval.x	$$⊢\phi \to X\in B$$
6		homaval.y	$$⊢\phi \to Y\in B$$
7		df-ov	$$⊢XHY=H\left(⟨X,Y⟩\right)$$
8	1 2 3 4	homafval	$$⊢\phi \to H=\left(z\in \left(B\times B\right)⟼\left\{z\right\}\times J\left(z\right)\right)$$
9		simpr	$$⊢\left(\phi \wedge z=⟨X,Y⟩\right)\to z=⟨X,Y⟩$$
10	9	sneqd	$$⊢\left(\phi \wedge z=⟨X,Y⟩\right)\to \left\{z\right\}=\left\{⟨X,Y⟩\right\}$$
11	9	fveq2d	$$⊢\left(\phi \wedge z=⟨X,Y⟩\right)\to J\left(z\right)=J\left(⟨X,Y⟩\right)$$
12		df-ov	$$⊢XJY=J\left(⟨X,Y⟩\right)$$
13	11 12	eqtr4di	$$⊢\left(\phi \wedge z=⟨X,Y⟩\right)\to J\left(z\right)=XJY$$
14	10 13	xpeq12d	$$⊢\left(\phi \wedge z=⟨X,Y⟩\right)\to \left\{z\right\}\times J\left(z\right)=\left\{⟨X,Y⟩\right\}\times \left(XJY\right)$$
15	5 6	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(B\times B\right)$$
16		snex	$$⊢\left\{⟨X,Y⟩\right\}\in \mathrm{V}$$
17		ovex	$$⊢XJY\in \mathrm{V}$$
18	16 17	xpex	$$⊢\left\{⟨X,Y⟩\right\}\times \left(XJY\right)\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to \left\{⟨X,Y⟩\right\}\times \left(XJY\right)\in \mathrm{V}$$
20	8 14 15 19	fvmptd	$$⊢\phi \to H\left(⟨X,Y⟩\right)=\left\{⟨X,Y⟩\right\}\times \left(XJY\right)$$
21	7 20	syl5eq	$$⊢\phi \to XHY=\left\{⟨X,Y⟩\right\}\times \left(XJY\right)$$