Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 18-Oct-2024)

	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	rescbas	$$⊢\phi \to S={\mathrm{Base}}_D$$

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		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
7		slotsbhcdif	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
8	7	simp1i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
9	6 8	setsnid	$$⊢{\mathrm{Base}}_{\left(C{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)}$$
10		eqid	$$⊢C{\upharpoonright }_{𝑠}S=C{\upharpoonright }_{𝑠}S$$
11	10 2	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_{\left(C{\upharpoonright }_{𝑠}S\right)}$$
12	5 11	syl	$$⊢\phi \to S={\mathrm{Base}}_{\left(C{\upharpoonright }_{𝑠}S\right)}$$
13	2	fvexi	$$⊢B\in \mathrm{V}$$
14	13	ssex	$$⊢S\subseteq B\to S\in \mathrm{V}$$
15	5 14	syl	$$⊢\phi \to S\in \mathrm{V}$$
16	1 3 15 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{Base}}_D={\mathrm{Base}}_{\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)}$$
18	9 12 17	3eqtr4a	$$⊢\phi \to S={\mathrm{Base}}_D$$