Theorem reschom

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	reschom	$$⊢\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		ovex	$$⊢C{\upharpoonright }_{𝑠}S\in \mathrm{V}$$
7	2	fvexi	$$⊢B\in \mathrm{V}$$
8	7	ssex	$$⊢S\subseteq B\to S\in \mathrm{V}$$
9	5 8	syl	$$⊢\phi \to S\in \mathrm{V}$$
10	9 9	xpexd	$$⊢\phi \to S\times S\in \mathrm{V}$$
11		fnex	$$⊢\left(HFn\left(S\times S\right)\wedge S\times S\in \mathrm{V}\right)\to H\in \mathrm{V}$$
12	4 10 11	syl2anc	$$⊢\phi \to H\in \mathrm{V}$$
13		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
14	13	setsid	$$⊢\left(C{\upharpoonright }_{𝑠}S\in \mathrm{V}\wedge H\in \mathrm{V}\right)\to H=\mathrm{Hom}\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)$$
15	6 12 14	sylancr	$$⊢\phi \to H=\mathrm{Hom}\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)$$
16	1 3 9 4	rescval2	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
17	16	fveq2d	$$⊢\phi \to \mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)$$
18	15 17	eqtr4d	$$⊢\phi \to H=\mathrm{Hom}\left(D\right)$$