Proof of Theorem rescabs
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢ (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾cat 𝐽) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉)
↾cat 𝐽) |
2 | | ovexd 6680 |
. . . 4
⊢ (𝜑 → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ∈
V) |
3 | | rescabs.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
4 | | rescabs.t |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ 𝑆) |
5 | 3, 4 | ssexd 4805 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ V) |
6 | | rescabs.j |
. . . 4
⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) |
7 | 1, 2, 5, 6 | rescval2 16488 |
. . 3
⊢ (𝜑 → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾cat
𝐽) = ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
8 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) |
9 | | ovexd 6680 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ∈
V) |
10 | 5 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ∈ V) |
11 | | eqid 2622 |
. . . . . . . 8
⊢ (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾s 𝑇) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉)
↾s 𝑇) |
12 | | baseid 15919 |
. . . . . . . . 9
⊢ Base =
Slot (Base‘ndx) |
13 | | 1re 10039 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
14 | | 1nn 11031 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
15 | | 4nn0 11311 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ0 |
16 | | 1nn0 11308 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
17 | | 1lt10 11681 |
. . . . . . . . . . . 12
⊢ 1 <
;10 |
18 | 14, 15, 16, 17 | declti 11546 |
. . . . . . . . . . 11
⊢ 1 <
;14 |
19 | 13, 18 | ltneii 10150 |
. . . . . . . . . 10
⊢ 1 ≠
;14 |
20 | | basendx 15923 |
. . . . . . . . . . 11
⊢
(Base‘ndx) = 1 |
21 | | homndx 16074 |
. . . . . . . . . . 11
⊢ (Hom
‘ndx) = ;14 |
22 | 20, 21 | neeq12i 2860 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (Hom ‘ndx) ↔ 1 ≠ ;14) |
23 | 19, 22 | mpbir 221 |
. . . . . . . . 9
⊢
(Base‘ndx) ≠ (Hom ‘ndx) |
24 | 12, 23 | setsnid 15915 |
. . . . . . . 8
⊢
(Base‘(𝐶
↾s 𝑆)) =
(Base‘((𝐶
↾s 𝑆) sSet
〈(Hom ‘ndx), 𝐻〉)) |
25 | 11, 24 | ressid2 15928 |
. . . . . . 7
⊢
(((Base‘(𝐶
↾s 𝑆))
⊆ 𝑇 ∧ ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉) ∈ V ∧
𝑇 ∈ V) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾s 𝑇) =
((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉)) |
26 | 8, 9, 10, 25 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) |
27 | 26 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉) sSet
〈(Hom ‘ndx), 𝐽〉)) |
28 | | ovex 6678 |
. . . . . 6
⊢ (𝐶 ↾s 𝑆) ∈ V |
29 | | xpexg 6960 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑇 ∈ V) → (𝑇 × 𝑇) ∈ V) |
30 | 5, 5, 29 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 × 𝑇) ∈ V) |
31 | | fnex 6481 |
. . . . . . . 8
⊢ ((𝐽 Fn (𝑇 × 𝑇) ∧ (𝑇 × 𝑇) ∈ V) → 𝐽 ∈ V) |
32 | 6, 30, 31 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ V) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝐽 ∈ V) |
34 | | setsabs 15902 |
. . . . . 6
⊢ (((𝐶 ↾s 𝑆) ∈ V ∧ 𝐽 ∈ V) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐽〉)) |
35 | 28, 33, 34 | sylancr 695 |
. . . . 5
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐽〉)) |
36 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ↾s 𝑆) = (𝐶 ↾s 𝑆) |
37 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐶) =
(Base‘𝐶) |
38 | 36, 37 | ressbas 15930 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑊 → (𝑆 ∩ (Base‘𝐶)) = (Base‘(𝐶 ↾s 𝑆))) |
39 | 3, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∩ (Base‘𝐶)) = (Base‘(𝐶 ↾s 𝑆))) |
40 | 39 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 ∩ (Base‘𝐶)) ⊆ 𝑇 ↔ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇)) |
41 | 40 | biimpar 502 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) ⊆ 𝑇) |
42 | | inss2 3834 |
. . . . . . . . . . 11
⊢ (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶) |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶)) |
44 | 41, 43 | ssind 3837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) ⊆ (𝑇 ∩ (Base‘𝐶))) |
45 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ⊆ 𝑆) |
46 | | ssrin 3838 |
. . . . . . . . . 10
⊢ (𝑇 ⊆ 𝑆 → (𝑇 ∩ (Base‘𝐶)) ⊆ (𝑆 ∩ (Base‘𝐶))) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑇 ∩ (Base‘𝐶)) ⊆ (𝑆 ∩ (Base‘𝐶))) |
48 | 44, 47 | eqssd 3620 |
. . . . . . . 8
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) = (𝑇 ∩ (Base‘𝐶))) |
49 | 48 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s (𝑆 ∩ (Base‘𝐶))) = (𝐶 ↾s (𝑇 ∩ (Base‘𝐶)))) |
50 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑆 ∈ 𝑊) |
51 | 37 | ressinbas 15936 |
. . . . . . . 8
⊢ (𝑆 ∈ 𝑊 → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
53 | 37 | ressinbas 15936 |
. . . . . . . 8
⊢ (𝑇 ∈ V → (𝐶 ↾s 𝑇) = (𝐶 ↾s (𝑇 ∩ (Base‘𝐶)))) |
54 | 10, 53 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑇) = (𝐶 ↾s (𝑇 ∩ (Base‘𝐶)))) |
55 | 49, 52, 54 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑆) = (𝐶 ↾s 𝑇)) |
56 | 55 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐽〉) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐽〉)) |
57 | 27, 35, 56 | 3eqtrd 2660 |
. . . 4
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
58 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) |
59 | | ovexd 6680 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ∈
V) |
60 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ∈ V) |
61 | 11, 24 | ressval2 15929 |
. . . . . . . 8
⊢ ((¬
(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 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) = (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) sSet
〈(Base‘ndx), (𝑇
∩ (Base‘(𝐶
↾s 𝑆)))〉)) |
63 | | ovexd 6680 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑆) ∈ V) |
64 | 23 | necomi 2848 |
. . . . . . . . 9
⊢ (Hom
‘ndx) ≠ (Base‘ndx) |
65 | 64 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (Hom ‘ndx) ≠
(Base‘ndx)) |
66 | | rescabs.h |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
67 | | xpexg 6960 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑊 ∧ 𝑆 ∈ 𝑊) → (𝑆 × 𝑆) ∈ V) |
68 | 3, 3, 67 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 × 𝑆) ∈ V) |
69 | | fnex 6481 |
. . . . . . . . . 10
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ (𝑆 × 𝑆) ∈ V) → 𝐻 ∈ V) |
70 | 66, 68, 69 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ V) |
71 | 70 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝐻 ∈ V) |
72 | | fvex 6201 |
. . . . . . . . . 10
⊢
(Base‘(𝐶
↾s 𝑆))
∈ V |
73 | 72 | inex2 4800 |
. . . . . . . . 9
⊢ (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆))) ∈ V |
74 | 73 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆))) ∈ V) |
75 | | fvex 6201 |
. . . . . . . . 9
⊢ (Hom
‘ndx) ∈ V |
76 | | fvex 6201 |
. . . . . . . . 9
⊢
(Base‘ndx) ∈ V |
77 | 75, 76 | setscom 15903 |
. . . . . . . 8
⊢ ((((𝐶 ↾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), 𝐻〉)) |
78 | 63, 65, 71, 74, 77 | syl22anc 1327 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) sSet
〈(Base‘ndx), (𝑇
∩ (Base‘(𝐶
↾s 𝑆)))〉) = (((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉) sSet 〈(Hom
‘ndx), 𝐻〉)) |
79 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ((𝐶 ↾s 𝑆) ↾s 𝑇) = ((𝐶 ↾s 𝑆) ↾s 𝑇) |
80 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘(𝐶
↾s 𝑆)) =
(Base‘(𝐶
↾s 𝑆)) |
81 | 79, 80 | ressval2 15929 |
. . . . . . . . . 10
⊢ ((¬
(Base‘(𝐶
↾s 𝑆))
⊆ 𝑇 ∧ (𝐶 ↾s 𝑆) ∈ V ∧ 𝑇 ∈ V) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = ((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉)) |
82 | 58, 63, 60, 81 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = ((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉)) |
83 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑆 ∈ 𝑊) |
84 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ⊆ 𝑆) |
85 | | ressabs 15939 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑊 ∧ 𝑇 ⊆ 𝑆) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = (𝐶 ↾s 𝑇)) |
86 | 83, 84, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = (𝐶 ↾s 𝑇)) |
87 | 82, 86 | eqtr3d 2658 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉) = (𝐶 ↾s 𝑇)) |
88 | 87 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉) sSet 〈(Hom
‘ndx), 𝐻〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐻〉)) |
89 | 62, 78, 88 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐻〉)) |
90 | 89 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
(((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐻〉) sSet
〈(Hom ‘ndx), 𝐽〉)) |
91 | | ovex 6678 |
. . . . . 6
⊢ (𝐶 ↾s 𝑇) ∈ V |
92 | 32 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝐽 ∈ V) |
93 | | setsabs 15902 |
. . . . . 6
⊢ (((𝐶 ↾s 𝑇) ∈ V ∧ 𝐽 ∈ V) → (((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx),
𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
94 | 91, 92, 93 | sylancr 695 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
95 | 90, 94 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
96 | 57, 95 | pm2.61dan 832 |
. . 3
⊢ (𝜑 → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
97 | 7, 96 | eqtrd 2656 |
. 2
⊢ (𝜑 → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾cat
𝐽) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐽〉)) |
98 | | eqid 2622 |
. . . 4
⊢ (𝐶 ↾cat 𝐻) = (𝐶 ↾cat 𝐻) |
99 | | rescabs.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
100 | 98, 99, 3, 66 | rescval2 16488 |
. . 3
⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) |
101 | 100 | oveq1d 6665 |
. 2
⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾cat
𝐽)) |
102 | | eqid 2622 |
. . 3
⊢ (𝐶 ↾cat 𝐽) = (𝐶 ↾cat 𝐽) |
103 | 102, 99, 5, 6 | rescval2 16488 |
. 2
⊢ (𝜑 → (𝐶 ↾cat 𝐽) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐽〉)) |
104 | 97, 101, 103 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) |