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 𝐽 ) )