# Metamath Proof Explorer

## Theorem rescabs

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

Ref Expression
Hypotheses rescabs.c ${⊢}{\phi }\to {C}\in {V}$
rescabs.h ${⊢}{\phi }\to {H}Fn\left({S}×{S}\right)$
rescabs.j ${⊢}{\phi }\to {J}Fn\left({T}×{T}\right)$
rescabs.s ${⊢}{\phi }\to {S}\in {W}$
rescabs.t ${⊢}{\phi }\to {T}\subseteq {S}$
Assertion rescabs ${⊢}{\phi }\to \left({C}{↾}_{\mathrm{cat}}{H}\right){↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$

### Proof

Step Hyp Ref Expression
1 rescabs.c ${⊢}{\phi }\to {C}\in {V}$
2 rescabs.h ${⊢}{\phi }\to {H}Fn\left({S}×{S}\right)$
3 rescabs.j ${⊢}{\phi }\to {J}Fn\left({T}×{T}\right)$
4 rescabs.s ${⊢}{\phi }\to {S}\in {W}$
5 rescabs.t ${⊢}{\phi }\to {T}\subseteq {S}$
6 eqid ${⊢}\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{\mathrm{cat}}{J}=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{\mathrm{cat}}{J}$
7 ovexd ${⊢}{\phi }\to \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\in \mathrm{V}$
8 4 5 ssexd ${⊢}{\phi }\to {T}\in \mathrm{V}$
9 6 7 8 3 rescval2 ${⊢}{\phi }\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{\mathrm{cat}}{J}=\left(\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
10 simpr ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}$
11 ovexd ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\in \mathrm{V}$
12 8 adantr ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {T}\in \mathrm{V}$
13 eqid ${⊢}\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}$
14 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
15 1re ${⊢}1\in ℝ$
16 1nn ${⊢}1\in ℕ$
17 4nn0 ${⊢}4\in {ℕ}_{0}$
18 1nn0 ${⊢}1\in {ℕ}_{0}$
19 1lt10 ${⊢}1<10$
20 16 17 18 19 declti ${⊢}1<14$
21 15 20 ltneii ${⊢}1\ne 14$
22 basendx ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}=1$
23 homndx ${⊢}\mathrm{Hom}\left(\mathrm{ndx}\right)=14$
24 22 23 neeq12i ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)↔1\ne 14$
25 21 24 mpbir ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$
26 14 25 setsnid ${⊢}{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}={\mathrm{Base}}_{\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)}$
27 13 26 ressid2 ${⊢}\left({\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\wedge \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
28 10 11 12 27 syl3anc ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
29 28 oveq1d ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
30 ovex ${⊢}{C}{↾}_{𝑠}{S}\in \mathrm{V}$
31 8 8 xpexd ${⊢}{\phi }\to {T}×{T}\in \mathrm{V}$
32 fnex ${⊢}\left({J}Fn\left({T}×{T}\right)\wedge {T}×{T}\in \mathrm{V}\right)\to {J}\in \mathrm{V}$
33 3 31 32 syl2anc ${⊢}{\phi }\to {J}\in \mathrm{V}$
34 33 adantr ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {J}\in \mathrm{V}$
35 setsabs ${⊢}\left({C}{↾}_{𝑠}{S}\in \mathrm{V}\wedge {J}\in \mathrm{V}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
36 30 34 35 sylancr ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
37 eqid ${⊢}{C}{↾}_{𝑠}{S}={C}{↾}_{𝑠}{S}$
38 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
39 37 38 ressbas ${⊢}{S}\in {W}\to {S}\cap {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}$
40 4 39 syl ${⊢}{\phi }\to {S}\cap {\mathrm{Base}}_{{C}}={\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}$
41 40 sseq1d ${⊢}{\phi }\to \left({S}\cap {\mathrm{Base}}_{{C}}\subseteq {T}↔{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)$
42 41 biimpar ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {S}\cap {\mathrm{Base}}_{{C}}\subseteq {T}$
43 inss2 ${⊢}{S}\cap {\mathrm{Base}}_{{C}}\subseteq {\mathrm{Base}}_{{C}}$
44 43 a1i ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {S}\cap {\mathrm{Base}}_{{C}}\subseteq {\mathrm{Base}}_{{C}}$
45 42 44 ssind ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {S}\cap {\mathrm{Base}}_{{C}}\subseteq {T}\cap {\mathrm{Base}}_{{C}}$
46 5 adantr ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {T}\subseteq {S}$
47 46 ssrind ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {T}\cap {\mathrm{Base}}_{{C}}\subseteq {S}\cap {\mathrm{Base}}_{{C}}$
48 45 47 eqssd ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {S}\cap {\mathrm{Base}}_{{C}}={T}\cap {\mathrm{Base}}_{{C}}$
49 48 oveq2d ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {C}{↾}_{𝑠}\left({S}\cap {\mathrm{Base}}_{{C}}\right)={C}{↾}_{𝑠}\left({T}\cap {\mathrm{Base}}_{{C}}\right)$
50 4 adantr ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {S}\in {W}$
51 38 ressinbas ${⊢}{S}\in {W}\to {C}{↾}_{𝑠}{S}={C}{↾}_{𝑠}\left({S}\cap {\mathrm{Base}}_{{C}}\right)$
52 50 51 syl ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {C}{↾}_{𝑠}{S}={C}{↾}_{𝑠}\left({S}\cap {\mathrm{Base}}_{{C}}\right)$
53 38 ressinbas ${⊢}{T}\in \mathrm{V}\to {C}{↾}_{𝑠}{T}={C}{↾}_{𝑠}\left({T}\cap {\mathrm{Base}}_{{C}}\right)$
54 12 53 syl ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {C}{↾}_{𝑠}{T}={C}{↾}_{𝑠}\left({T}\cap {\mathrm{Base}}_{{C}}\right)$
55 49 52 54 3eqtr4d ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {C}{↾}_{𝑠}{S}={C}{↾}_{𝑠}{T}$
56 55 oveq1d ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
57 29 36 56 3eqtrd ${⊢}\left({\phi }\wedge {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
58 simpr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}$
59 ovexd ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\in \mathrm{V}$
60 8 adantr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {T}\in \mathrm{V}$
61 13 26 ressval2 ${⊢}\left(¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\wedge \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩$
62 58 59 60 61 syl3anc ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩$
63 ovexd ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {C}{↾}_{𝑠}{S}\in \mathrm{V}$
64 25 necomi ${⊢}\mathrm{Hom}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$
65 64 a1i ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \mathrm{Hom}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$
66 4 4 xpexd ${⊢}{\phi }\to {S}×{S}\in \mathrm{V}$
67 fnex ${⊢}\left({H}Fn\left({S}×{S}\right)\wedge {S}×{S}\in \mathrm{V}\right)\to {H}\in \mathrm{V}$
68 2 66 67 syl2anc ${⊢}{\phi }\to {H}\in \mathrm{V}$
69 68 adantr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {H}\in \mathrm{V}$
70 fvex ${⊢}{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\in \mathrm{V}$
71 70 inex2 ${⊢}{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\in \mathrm{V}$
72 71 a1i ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\in \mathrm{V}$
73 fvex ${⊢}\mathrm{Hom}\left(\mathrm{ndx}\right)\in \mathrm{V}$
74 fvex ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$
75 73 74 setscom ${⊢}\left(\left({C}{↾}_{𝑠}{S}\in \mathrm{V}\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\right)\wedge \left({H}\in \mathrm{V}\wedge {T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\in \mathrm{V}\right)\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
76 63 65 69 72 75 syl22anc ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
77 eqid ${⊢}\left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}=\left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}$
78 eqid ${⊢}{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}={\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}$
79 77 78 ressval2 ${⊢}\left(¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\wedge {C}{↾}_{𝑠}{S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\to \left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩$
80 58 63 60 79 syl3anc ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩$
81 4 adantr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {S}\in {W}$
82 5 adantr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {T}\subseteq {S}$
83 ressabs ${⊢}\left({S}\in {W}\wedge {T}\subseteq {S}\right)\to \left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}={C}{↾}_{𝑠}{T}$
84 81 82 83 syl2anc ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left({C}{↾}_{𝑠}{S}\right){↾}_{𝑠}{T}={C}{↾}_{𝑠}{T}$
85 80 84 eqtr3d ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩={C}{↾}_{𝑠}{T}$
86 85 oveq1d ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{T}\cap {\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
87 62 76 86 3eqtrd ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
88 87 oveq1d ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left(\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
89 ovex ${⊢}{C}{↾}_{𝑠}{T}\in \mathrm{V}$
90 33 adantr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to {J}\in \mathrm{V}$
91 setsabs ${⊢}\left({C}{↾}_{𝑠}{T}\in \mathrm{V}\wedge {J}\in \mathrm{V}\right)\to \left(\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
92 89 90 91 sylancr ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
93 88 92 eqtrd ${⊢}\left({\phi }\wedge ¬{\mathrm{Base}}_{\left({C}{↾}_{𝑠}{S}\right)}\subseteq {T}\right)\to \left(\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
94 57 93 pm2.61dan ${⊢}{\phi }\to \left(\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
95 9 94 eqtrd ${⊢}{\phi }\to \left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{\mathrm{cat}}{J}=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
96 eqid ${⊢}{C}{↾}_{\mathrm{cat}}{H}={C}{↾}_{\mathrm{cat}}{H}$
97 96 1 4 2 rescval2 ${⊢}{\phi }\to {C}{↾}_{\mathrm{cat}}{H}=\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩$
98 97 oveq1d ${⊢}{\phi }\to \left({C}{↾}_{\mathrm{cat}}{H}\right){↾}_{\mathrm{cat}}{J}=\left(\left({C}{↾}_{𝑠}{S}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{H}⟩\right){↾}_{\mathrm{cat}}{J}$
99 eqid ${⊢}{C}{↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$
100 99 1 8 3 rescval2 ${⊢}{\phi }\to {C}{↾}_{\mathrm{cat}}{J}=\left({C}{↾}_{𝑠}{T}\right)\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{J}⟩$
101 95 98 100 3eqtr4d ${⊢}{\phi }\to \left({C}{↾}_{\mathrm{cat}}{H}\right){↾}_{\mathrm{cat}}{J}={C}{↾}_{\mathrm{cat}}{J}$