Theorem rescco

Description: Composition in 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$$
	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		1nn0	$$⊢1\in {\mathbb{N}}_0$$
9		4nn	$$⊢4\in \mathbb{N}$$
10	8 9	decnncl	$$⊢14\in \mathbb{N}$$
11	10	nnrei	$$⊢14\in ℝ$$
12		4nn0	$$⊢4\in {\mathbb{N}}_0$$
13		5nn	$$⊢5\in \mathbb{N}$$
14		4lt5	$$⊢4<5$$
15	8 12 13 14	declt	$$⊢14<15$$
16	11 15	gtneii	$$⊢15\ne 14$$
17		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
18		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
19	17 18	neeq12i	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 15\ne 14$$
20	16 19	mpbir	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
21	7 20	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)$$
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		eqid	$$⊢C{\upharpoonright }_{𝑠}S=C{\upharpoonright }_{𝑠}S$$
26	25 6	ressco	$$⊢S\in \mathrm{V}\to \underset{\dot{}}{·}=\mathrm{comp}\left(C{\upharpoonright }_{𝑠}S\right)$$
27	24 26	syl	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(C{\upharpoonright }_{𝑠}S\right)$$
28	1 3 24 4	rescval2	$$⊢\phi \to D=\left(C{\upharpoonright }_{𝑠}S\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩$$
29	28	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)$$
30	21 27 29	3eqtr4a	$$⊢\phi \to \underset{\dot{}}{·}=\mathrm{comp}\left(D\right)$$