Theorem rescval2

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

	Ref	Expression
Hypotheses	rescval.1	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}H$$
	rescval2.1	$$⊢\phi \to C\in V$$
	rescval2.2	$$⊢\phi \to S\in W$$
	rescval2.3	$$⊢\phi \to HFn\left(S\times S\right)$$
Assertion	rescval2	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$

Proof

Step	Hyp	Ref	Expression
1		rescval.1	$$⊢D=C{\upharpoonright }_{\mathrm{cat}}H$$
2		rescval2.1	$$⊢\phi \to C\in V$$
3		rescval2.2	$$⊢\phi \to S\in W$$
4		rescval2.3	$$⊢\phi \to HFn\left(S\times S\right)$$
5	3 3	xpexd	$$⊢\phi \to S\times S\in \mathrm{V}$$
6		fnex	$$⊢\left(HFn\left(S\times S\right)\wedge S\times S\in \mathrm{V}\right)\to H\in \mathrm{V}$$
7	4 5 6	syl2anc	$$⊢\phi \to H\in \mathrm{V}$$
8	1	rescval	$$⊢\left(C\in V\wedge H\in \mathrm{V}\right)\to D=\left(C{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{dom}H\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
9	2 7 8	syl2anc	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{dom}H\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
10	4	fndmd	$$⊢\phi \to \mathrm{dom}H=S\times S$$
11	10	dmeqd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}H=\mathrm{dom}\left(S\times S\right)$$
12		dmxpid	$$⊢\mathrm{dom}\left(S\times S\right)=S$$
13	11 12	eqtrdi	$$⊢\phi \to \mathrm{dom}\mathrm{dom}H=S$$
14	13	oveq2d	$$⊢\phi \to C{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{dom}H=C{\upharpoonright }_{𝑠}S$$
15	14	oveq1d	$$⊢\phi \to \left(C{\upharpoonright }_{𝑠}\mathrm{dom}\mathrm{dom}H\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
16	9 15	eqtrd	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$