Theorem rescco

Description: Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 13-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$$
	rescco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
Assertion	rescco	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\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		rescco.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
7		ccoid	$$⊢\mathrm{comp}=\mathrm{Slot}\mathrm{comp}\left(\mathrm{ndx}\right)$$
8		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)$$
9		simp3	$$⊢\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)\to \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
10	9	necomd	$$⊢\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)\to \mathrm{comp}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
11	8 10	ax-mp	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
12	7 11	setsnid	$$⊢\mathrm{comp}\left(C{\upharpoonright }_{𝑠}S\right)=\mathrm{comp}\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\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		eqid	$$⊢C{\upharpoonright }_{𝑠}S=C{\upharpoonright }_{𝑠}S$$
17	16 6	ressco	$$⊢S\in \mathrm{V}\to \underset{\dot{}}{·}=\mathrm{comp}\left(C{\upharpoonright }_{𝑠}S\right)$$
18	15 17	syl	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(C{\upharpoonright }_{𝑠}S\right)$$
19	1 3 15 4	rescval2	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
20	19	fveq2d	$$⊢\phi \to \mathrm{comp}\left(D\right)=\mathrm{comp}\left(\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩\right)$$
21	12 18 20	3eqtr4a	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$