# Metamath Proof Explorer

## Theorem rescabs

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

Ref Expression
Hypotheses rescabs.c ( 𝜑𝐶𝑉 )
rescabs.h ( 𝜑𝐻 Fn ( 𝑆 × 𝑆 ) )
rescabs.j ( 𝜑𝐽 Fn ( 𝑇 × 𝑇 ) )
rescabs.s ( 𝜑𝑆𝑊 )
rescabs.t ( 𝜑𝑇𝑆 )
Assertion rescabs ( 𝜑 → ( ( 𝐶cat 𝐻 ) ↾cat 𝐽 ) = ( 𝐶cat 𝐽 ) )

### Proof

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