Theorem reschomf

Description: Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	rescbas.d	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}H$$
	rescbas.b	$$⊢B={\mathrm{Base}}_C$$
	rescbas.c	$$⊢\phi \to C\in V$$
	rescbas.h	$$⊢\phi \to HFn\left(S\times S\right)$$
	rescbas.s	$$⊢\phi \to S\subseteq B$$
Assertion	reschomf	$$⊢\phi \to H={\mathrm{Hom}}_{𝑓}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		rescbas.d	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}H$$
2		rescbas.b	$$⊢B={\mathrm{Base}}_C$$
3		rescbas.c	$$⊢\phi \to C\in V$$
4		rescbas.h	$$⊢\phi \to HFn\left(S\times S\right)$$
5		rescbas.s	$$⊢\phi \to S\subseteq B$$
6	1 2 3 4 5	reschom	$$⊢\phi \to H=\mathrm{Hom}\left(D\right)$$
7	1 2 3 4 5	rescbas	$$⊢\phi \to S={\mathrm{Base}}_D$$
8	7	sqxpeqd	$$⊢\phi \to S\times S={\mathrm{Base}}_D\times {\mathrm{Base}}_D$$
9	6 8	fneq12d	$$⊢\phi \to \left(HFn\left(S\times S\right)\leftrightarrow \mathrm{Hom}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)\right)$$
10	4 9	mpbid	$$⊢\phi \to \mathrm{Hom}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
11		fnov	$$⊢\mathrm{Hom}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)\leftrightarrow \mathrm{Hom}\left(D\right)=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼x\mathrm{Hom}\left(D\right)y\right)$$
12	10 11	sylib	$$⊢\phi \to \mathrm{Hom}\left(D\right)=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼x\mathrm{Hom}\left(D\right)y\right)$$
13	6 12	eqtrd	$$⊢\phi \to H=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼x\mathrm{Hom}\left(D\right)y\right)$$
14		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
15		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
16		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
17	14 15 16	homffval	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼x\mathrm{Hom}\left(D\right)y\right)$$
18	13 17	eqtr4di	$$⊢\phi \to H={\mathrm{Hom}}_{𝑓}\left(D\right)$$