This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rescabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 9-Nov-2024)

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 slotsbhcdif ⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
16 15 simp1i ⊢ ( Base ‘ ndx ) ≠ ( Hom ‘ ndx )
17 14 16 setsnid ⊢ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) = ( Base ‘ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
18 13 17 ressid2 ⊢ ( ( ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ∧ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ∈ V ∧ 𝑇 ∈ V ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
19 10 11 12 18 syl3anc ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
20 19 oveq1d ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
21 ovex ⊢ ( 𝐶 ↾s 𝑆 ) ∈ V
22 8 8 xpexd ⊢ ( 𝜑 → ( 𝑇 × 𝑇 ) ∈ V )
23 3 22 fnexd ⊢ ( 𝜑 → 𝐽 ∈ V )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝐽 ∈ V )
25 setsabs ⊢ ( ( ( 𝐶 ↾s 𝑆 ) ∈ V ∧ 𝐽 ∈ V ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
26 21 24 25 sylancr ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
27 eqid ⊢ ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s 𝑆 )
28 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
29 27 28 ressbas ⊢ ( 𝑆 ∈ 𝑊 → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) = ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) )
30 4 29 syl ⊢ ( 𝜑 → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) = ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) )
31 30 sseq1d ⊢ ( 𝜑 → ( ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ 𝑇 ↔ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) )
32 31 biimpar ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ 𝑇 )
33 inss2 ⊢ ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐶 )
34 33 a1i ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( Base ‘ 𝐶 ) )
35 32 34 ssind ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( 𝑇 ∩ ( Base ‘ 𝐶 ) ) )
36 5 adantr ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝑇 ⊆ 𝑆 )
37 36 ssrind ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝑇 ∩ ( Base ‘ 𝐶 ) ) ⊆ ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) )
38 35 37 eqssd ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) = ( 𝑇 ∩ ( Base ‘ 𝐶 ) ) )
39 38 oveq2d ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) = ( 𝐶 ↾s ( 𝑇 ∩ ( Base ‘ 𝐶 ) ) ) )
40 4 adantr ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝑆 ∈ 𝑊 )
41 28 ressinbas ⊢ ( 𝑆 ∈ 𝑊 → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
42 40 41 syl ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s ( 𝑆 ∩ ( Base ‘ 𝐶 ) ) ) )
43 28 ressinbas ⊢ ( 𝑇 ∈ V → ( 𝐶 ↾s 𝑇 ) = ( 𝐶 ↾s ( 𝑇 ∩ ( Base ‘ 𝐶 ) ) ) )
44 12 43 syl ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝐶 ↾s 𝑇 ) = ( 𝐶 ↾s ( 𝑇 ∩ ( Base ‘ 𝐶 ) ) ) )
45 39 42 44 3eqtr4d ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝐶 ↾s 𝑆 ) = ( 𝐶 ↾s 𝑇 ) )
46 45 oveq1d ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
47 20 26 46 3eqtrd ⊢ ( ( 𝜑 ∧ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
48 simpr ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 )
49 ovexd ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ∈ V )
50 8 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝑇 ∈ V )
51 13 17 ressval2 ⊢ ( ( ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ∧ ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ∈ V ∧ 𝑇 ∈ V ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) = ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) )
52 48 49 50 51 syl3anc ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) = ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) )
53 ovexd ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝐶 ↾s 𝑆 ) ∈ V )
54 16 necomi ⊢ ( Hom ‘ ndx ) ≠ ( Base ‘ ndx )
55 54 a1i ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( Hom ‘ ndx ) ≠ ( Base ‘ ndx ) )
56 4 4 xpexd ⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ V )
57 2 56 fnexd ⊢ ( 𝜑 → 𝐻 ∈ V )
58 57 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝐻 ∈ V )
59 fvex ⊢ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ∈ V
60 59 inex2 ⊢ ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ∈ V
61 60 a1i ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ∈ V )
62 fvex ⊢ ( Hom ‘ ndx ) ∈ V
63 fvex ⊢ ( Base ‘ ndx ) ∈ V
64 62 63 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 ) , 𝐻 ⟩ ) )
65 53 55 58 61 64 syl22anc ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) = ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
66 eqid ⊢ ( ( 𝐶 ↾s 𝑆 ) ↾s 𝑇 ) = ( ( 𝐶 ↾s 𝑆 ) ↾s 𝑇 )
67 eqid ⊢ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐶 ↾s 𝑆 ) )
68 66 67 ressval2 ⊢ ( ( ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ∧ ( 𝐶 ↾s 𝑆 ) ∈ V ∧ 𝑇 ∈ V ) → ( ( 𝐶 ↾s 𝑆 ) ↾s 𝑇 ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) )
69 48 53 50 68 syl3anc ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( 𝐶 ↾s 𝑆 ) ↾s 𝑇 ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) )
70 5 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝑇 ⊆ 𝑆 )
71 ressabs ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝑇 ⊆ 𝑆 ) → ( ( 𝐶 ↾s 𝑆 ) ↾s 𝑇 ) = ( 𝐶 ↾s 𝑇 ) )
72 4 70 71 syl2an2r ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( 𝐶 ↾s 𝑆 ) ↾s 𝑇 ) = ( 𝐶 ↾s 𝑇 ) )
73 69 72 eqtr3d ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) = ( 𝐶 ↾s 𝑇 ) )
74 73 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝑇 ∩ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ) ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
75 52 65 74 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
76 75 oveq1d ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
77 ovex ⊢ ( 𝐶 ↾s 𝑇 ) ∈ V
78 23 adantr ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → 𝐽 ∈ V )
79 setsabs ⊢ ( ( ( 𝐶 ↾s 𝑇 ) ∈ V ∧ 𝐽 ∈ V ) → ( ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
80 77 78 79 sylancr ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
81 76 80 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( Base ‘ ( 𝐶 ↾s 𝑆 ) ) ⊆ 𝑇 ) → ( ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
82 47 81 pm2.61dan ⊢ ( 𝜑 → ( ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
83 9 82 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾cat 𝐽 ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
84 eqid ⊢ ( 𝐶 ↾cat 𝐻 ) = ( 𝐶 ↾cat 𝐻 )
85 84 1 4 2 rescval2 ⊢ ( 𝜑 → ( 𝐶 ↾cat 𝐻 ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
86 85 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 ↾cat 𝐻 ) ↾cat 𝐽 ) = ( ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ↾cat 𝐽 ) )
87 eqid ⊢ ( 𝐶 ↾cat 𝐽 ) = ( 𝐶 ↾cat 𝐽 )
88 87 1 8 3 rescval2 ⊢ ( 𝜑 → ( 𝐶 ↾cat 𝐽 ) = ( ( 𝐶 ↾s 𝑇 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐽 ⟩ ) )
89 83 86 88 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐶 ↾cat 𝐻 ) ↾cat 𝐽 ) = ( 𝐶 ↾cat 𝐽 ) )