Theorem homafval

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}$$
	homafval.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
Assertion	homafval	$$⊢\phi \to H=\left(x\in \left(B\times B\right)⟼\left\{x\right\}\times J\left(x\right)\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		homafval.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
5		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
6	5 2	eqtr4di	$$⊢c=C\to {\mathrm{Base}}_c=B$$
7	6	sqxpeqd	$$⊢c=C\to {\mathrm{Base}}_c\times {\mathrm{Base}}_c=B\times B$$
8		fveq2	$$⊢c=C\to \mathrm{Hom}\left(c\right)=\mathrm{Hom}\left(C\right)$$
9	8 4	eqtr4di	$$⊢c=C\to \mathrm{Hom}\left(c\right)=J$$
10	9	fveq1d	$$⊢c=C\to \mathrm{Hom}\left(c\right)\left(x\right)=J\left(x\right)$$
11	10	xpeq2d	$$⊢c=C\to \left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)=\left\{x\right\}\times J\left(x\right)$$
12	7 11	mpteq12dv	$$⊢c=C\to \left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)⟼\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)=\left(x\in \left(B\times B\right)⟼\left\{x\right\}\times J\left(x\right)\right)$$
13		df-homa	$$⊢{Hom}_a=\left(c\in \mathrm{Cat}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)⟼\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)\right)$$
14	2	fvexi	$$⊢B\in \mathrm{V}$$
15	14 14	xpex	$$⊢B\times B\in \mathrm{V}$$
16	15	mptex	$$⊢\left(x\in \left(B\times B\right)⟼\left\{x\right\}\times J\left(x\right)\right)\in \mathrm{V}$$
17	12 13 16	fvmpt	$$⊢C\in \mathrm{Cat}\to {Hom}_a\left(C\right)=\left(x\in \left(B\times B\right)⟼\left\{x\right\}\times J\left(x\right)\right)$$
18	3 17	syl	$$⊢\phi \to {Hom}_a\left(C\right)=\left(x\in \left(B\times B\right)⟼\left\{x\right\}\times J\left(x\right)\right)$$
19	1 18	eqtrid	$$⊢\phi \to H=\left(x\in \left(B\times B\right)⟼\left\{x\right\}\times J\left(x\right)\right)$$