Theorem rescabs2

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	rescabs2.c	$$⊢\phi \to C\in V$$
	rescabs2.j	$$⊢\phi \to JFn\left(T\times T\right)$$
	rescabs2.s	$$⊢\phi \to S\in W$$
	rescabs2.t	$$⊢\phi \to T\subseteq S$$
Assertion	rescabs2	$$⊢\phi \to \left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{\mathrm{cat}}J=C{\upharpoonright }_{\mathrm{cat}}J$$

Proof

Step	Hyp	Ref	Expression
1		rescabs2.c	$$⊢\phi \to C\in V$$
2		rescabs2.j	$$⊢\phi \to JFn\left(T\times T\right)$$
3		rescabs2.s	$$⊢\phi \to S\in W$$
4		rescabs2.t	$$⊢\phi \to T\subseteq S$$
5		ressabs	$$⊢\left(S\in W\wedge T\subseteq S\right)\to \left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{𝑠}T=C{\upharpoonright }_{𝑠}T$$
6	3 4 5	syl2anc	$$⊢\phi \to \left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{𝑠}T=C{\upharpoonright }_{𝑠}T$$
7	6	oveq1d	$$⊢\phi \to \left(\left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{𝑠}T\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),J⟩=\left(C{\upharpoonright }_{𝑠}T\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),J⟩$$
8		eqid	$$⊢\left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{\mathrm{cat}}J=\left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{\mathrm{cat}}J$$
9		ovexd	$$⊢\phi \to C{\upharpoonright }_{𝑠}S\in \mathrm{V}$$
10	3 4	ssexd	$$⊢\phi \to T\in \mathrm{V}$$
11	8 9 10 2	rescval2	$$⊢\phi \to \left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{\mathrm{cat}}J=\left(\left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{𝑠}T\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),J⟩$$
12		eqid	$$⊢C{\upharpoonright }_{\mathrm{cat}}J=C{\upharpoonright }_{\mathrm{cat}}J$$
13	12 1 10 2	rescval2	$$⊢\phi \to C{\upharpoonright }_{\mathrm{cat}}J=\left(C{\upharpoonright }_{𝑠}T\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),J⟩$$
14	7 11 13	3eqtr4d	$$⊢\phi \to \left(C{\upharpoonright }_{𝑠}S\right){\upharpoonright }_{\mathrm{cat}}J=C{\upharpoonright }_{\mathrm{cat}}J$$