Theorem rescbasOLD

Description: Obsolete version of rescbas as of 18-Oct-2024. Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	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	rescbasOLD	$$⊢\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		1re	$$⊢1\in ℝ$$
8		1nn	$$⊢1\in \mathbb{N}$$
9		4nn0	$$⊢4\in {\mathbb{N}}_0$$
10		1nn0	$$⊢1\in {\mathbb{N}}_0$$
11		1lt10	$$⊢1<10$$
12	8 9 10 11	declti	$$⊢1<14$$
13	7 12	ltneii	$$⊢1\ne 14$$
14		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
15		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
16	14 15	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 14$$
17	13 16	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
18	6 17	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)}$$
19		eqid	$$⊢C{\upharpoonright }_{𝑠}S=C{\upharpoonright }_{𝑠}S$$
20	19 2	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_{\left(C{\upharpoonright }_{𝑠}S\right)}$$
21	5 20	syl	$$⊢\phi \to S={\mathrm{Base}}_{\left(C{\upharpoonright }_{𝑠}S\right)}$$
22	2	fvexi	$$⊢B\in \mathrm{V}$$
23	22	ssex	$$⊢S\subseteq B\to S\in \mathrm{V}$$
24	5 23	syl	$$⊢\phi \to S\in \mathrm{V}$$
25	1 3 24 4	rescval2	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
26	25	fveq2d	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_{\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)}$$
27	18 21 26	3eqtr4a	$$⊢\phi \to S={\mathrm{Base}}_D$$