Proof of Theorem rescabs
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢ (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾cat 𝐽) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉)
↾cat 𝐽) |
2 | | ovex 6577 |
. . . . 5
⊢ ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉) ∈
V |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ∈
V) |
4 | | rescabs.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
5 | | rescabs.t |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ 𝑆) |
6 | 4, 5 | ssexd 4733 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ V) |
7 | | rescabs.j |
. . . 4
⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) |
8 | 1, 3, 6, 7 | rescval2 16311 |
. . 3
⊢ (𝜑 → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾cat
𝐽) = ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
9 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) |
10 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ∈
V) |
11 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ∈ V) |
12 | | eqid 2610 |
. . . . . . . 8
⊢ (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾s 𝑇) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉)
↾s 𝑇) |
13 | | baseid 15747 |
. . . . . . . . 9
⊢ Base =
Slot (Base‘ndx) |
14 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
15 | | 1nn 10908 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
16 | | 4nn0 11188 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ0 |
17 | | 1nn0 11185 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
18 | | 1lt10 11557 |
. . . . . . . . . . . 12
⊢ 1 <
;10 |
19 | 15, 16, 17, 18 | declti 11422 |
. . . . . . . . . . 11
⊢ 1 <
;14 |
20 | 14, 19 | ltneii 10029 |
. . . . . . . . . 10
⊢ 1 ≠
;14 |
21 | | basendx 15751 |
. . . . . . . . . . 11
⊢
(Base‘ndx) = 1 |
22 | | homndx 15897 |
. . . . . . . . . . 11
⊢ (Hom
‘ndx) = ;14 |
23 | 21, 22 | neeq12i 2848 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (Hom ‘ndx) ↔ 1 ≠ ;14) |
24 | 20, 23 | mpbir 220 |
. . . . . . . . 9
⊢
(Base‘ndx) ≠ (Hom ‘ndx) |
25 | 13, 24 | setsnid 15743 |
. . . . . . . 8
⊢
(Base‘(𝐶
↾s 𝑆)) =
(Base‘((𝐶
↾s 𝑆) sSet
〈(Hom ‘ndx), 𝐻〉)) |
26 | 12, 25 | ressid2 15755 |
. . . . . . 7
⊢
(((Base‘(𝐶
↾s 𝑆))
⊆ 𝑇 ∧ ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉) ∈ V ∧
𝑇 ∈ V) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾s 𝑇) =
((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉)) |
27 | 9, 10, 11, 26 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) |
28 | 27 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉) sSet
〈(Hom ‘ndx), 𝐽〉)) |
29 | | ovex 6577 |
. . . . . 6
⊢ (𝐶 ↾s 𝑆) ∈ V |
30 | | xpexg 6858 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑇 ∈ V) → (𝑇 × 𝑇) ∈ V) |
31 | 6, 6, 30 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 × 𝑇) ∈ V) |
32 | | fnex 6386 |
. . . . . . . 8
⊢ ((𝐽 Fn (𝑇 × 𝑇) ∧ (𝑇 × 𝑇) ∈ V) → 𝐽 ∈ V) |
33 | 7, 31, 32 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ V) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝐽 ∈ V) |
35 | | setsabs 15730 |
. . . . . 6
⊢ (((𝐶 ↾s 𝑆) ∈ V ∧ 𝐽 ∈ V) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐽〉)) |
36 | 29, 34, 35 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐽〉)) |
37 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ↾s 𝑆) = (𝐶 ↾s 𝑆) |
38 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐶) =
(Base‘𝐶) |
39 | 37, 38 | ressbas 15757 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑊 → (𝑆 ∩ (Base‘𝐶)) = (Base‘(𝐶 ↾s 𝑆))) |
40 | 4, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∩ (Base‘𝐶)) = (Base‘(𝐶 ↾s 𝑆))) |
41 | 40 | sseq1d 3595 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 ∩ (Base‘𝐶)) ⊆ 𝑇 ↔ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇)) |
42 | 41 | biimpar 501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) ⊆ 𝑇) |
43 | | inss2 3796 |
. . . . . . . . . . 11
⊢ (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶) |
44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶)) |
45 | 42, 44 | ssind 3799 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) ⊆ (𝑇 ∩ (Base‘𝐶))) |
46 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ⊆ 𝑆) |
47 | | ssrin 3800 |
. . . . . . . . . 10
⊢ (𝑇 ⊆ 𝑆 → (𝑇 ∩ (Base‘𝐶)) ⊆ (𝑆 ∩ (Base‘𝐶))) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑇 ∩ (Base‘𝐶)) ⊆ (𝑆 ∩ (Base‘𝐶))) |
49 | 45, 48 | eqssd 3585 |
. . . . . . . 8
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑆 ∩ (Base‘𝐶)) = (𝑇 ∩ (Base‘𝐶))) |
50 | 49 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s (𝑆 ∩ (Base‘𝐶))) = (𝐶 ↾s (𝑇 ∩ (Base‘𝐶)))) |
51 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑆 ∈ 𝑊) |
52 | 38 | ressinbas 15763 |
. . . . . . . 8
⊢ (𝑆 ∈ 𝑊 → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
53 | 51, 52 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
54 | 38 | ressinbas 15763 |
. . . . . . . 8
⊢ (𝑇 ∈ V → (𝐶 ↾s 𝑇) = (𝐶 ↾s (𝑇 ∩ (Base‘𝐶)))) |
55 | 11, 54 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑇) = (𝐶 ↾s (𝑇 ∩ (Base‘𝐶)))) |
56 | 50, 53, 55 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑆) = (𝐶 ↾s 𝑇)) |
57 | 56 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐽〉) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐽〉)) |
58 | 28, 36, 57 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
59 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) |
60 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ∈
V) |
61 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ∈ V) |
62 | 12, 25 | ressval2 15756 |
. . . . . . . 8
⊢ ((¬
(Base‘(𝐶
↾s 𝑆))
⊆ 𝑇 ∧ ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉) ∈ V ∧
𝑇 ∈ V) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx),
𝐻〉)
↾s 𝑇) =
(((𝐶 ↾s
𝑆) sSet 〈(Hom
‘ndx), 𝐻〉) sSet
〈(Base‘ndx), (𝑇
∩ (Base‘(𝐶
↾s 𝑆)))〉)) |
63 | 59, 60, 61, 62 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) = (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) sSet
〈(Base‘ndx), (𝑇
∩ (Base‘(𝐶
↾s 𝑆)))〉)) |
64 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝐶 ↾s 𝑆) ∈ V) |
65 | 24 | necomi 2836 |
. . . . . . . . 9
⊢ (Hom
‘ndx) ≠ (Base‘ndx) |
66 | 65 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (Hom ‘ndx) ≠
(Base‘ndx)) |
67 | | rescabs.h |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
68 | | xpexg 6858 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑊 ∧ 𝑆 ∈ 𝑊) → (𝑆 × 𝑆) ∈ V) |
69 | 4, 4, 68 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 × 𝑆) ∈ V) |
70 | | fnex 6386 |
. . . . . . . . . 10
⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ (𝑆 × 𝑆) ∈ V) → 𝐻 ∈ V) |
71 | 67, 69, 70 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ V) |
72 | 71 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝐻 ∈ V) |
73 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘(𝐶
↾s 𝑆))
∈ V |
74 | 73 | inex2 4728 |
. . . . . . . . 9
⊢ (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆))) ∈ V |
75 | 74 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆))) ∈ V) |
76 | | fvex 6113 |
. . . . . . . . 9
⊢ (Hom
‘ndx) ∈ V |
77 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘ndx) ∈ V |
78 | 76, 77 | setscom 15731 |
. . . . . . . 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), 𝐻〉)) |
79 | 64, 66, 72, 75, 78 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) sSet
〈(Base‘ndx), (𝑇
∩ (Base‘(𝐶
↾s 𝑆)))〉) = (((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉) sSet 〈(Hom
‘ndx), 𝐻〉)) |
80 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ((𝐶 ↾s 𝑆) ↾s 𝑇) = ((𝐶 ↾s 𝑆) ↾s 𝑇) |
81 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘(𝐶
↾s 𝑆)) =
(Base‘(𝐶
↾s 𝑆)) |
82 | 80, 81 | ressval2 15756 |
. . . . . . . . . 10
⊢ ((¬
(Base‘(𝐶
↾s 𝑆))
⊆ 𝑇 ∧ (𝐶 ↾s 𝑆) ∈ V ∧ 𝑇 ∈ V) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = ((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉)) |
83 | 59, 64, 61, 82 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = ((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉)) |
84 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑆 ∈ 𝑊) |
85 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝑇 ⊆ 𝑆) |
86 | | ressabs 15766 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑊 ∧ 𝑇 ⊆ 𝑆) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = (𝐶 ↾s 𝑇)) |
87 | 84, 85, 86 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) ↾s 𝑇) = (𝐶 ↾s 𝑇)) |
88 | 83, 87 | eqtr3d 2646 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉) = (𝐶 ↾s 𝑇)) |
89 | 88 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Base‘ndx), (𝑇 ∩ (Base‘(𝐶 ↾s 𝑆)))〉) sSet 〈(Hom
‘ndx), 𝐻〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐻〉)) |
90 | 63, 79, 89 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐻〉)) |
91 | 90 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
(((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐻〉) sSet
〈(Hom ‘ndx), 𝐽〉)) |
92 | | ovex 6577 |
. . . . . 6
⊢ (𝐶 ↾s 𝑇) ∈ V |
93 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → 𝐽 ∈ V) |
94 | | setsabs 15730 |
. . . . . 6
⊢ (((𝐶 ↾s 𝑇) ∈ V ∧ 𝐽 ∈ V) → (((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx),
𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
95 | 92, 93, 94 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → (((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐻〉) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
96 | 91, 95 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ ¬ (Base‘(𝐶 ↾s 𝑆)) ⊆ 𝑇) → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
97 | 58, 96 | pm2.61dan 828 |
. . 3
⊢ (𝜑 → ((((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉) =
((𝐶 ↾s
𝑇) sSet 〈(Hom
‘ndx), 𝐽〉)) |
98 | 8, 97 | eqtrd 2644 |
. 2
⊢ (𝜑 → (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾cat
𝐽) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐽〉)) |
99 | | eqid 2610 |
. . . 4
⊢ (𝐶 ↾cat 𝐻) = (𝐶 ↾cat 𝐻) |
100 | | rescabs.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
101 | 99, 100, 4, 67 | rescval2 16311 |
. . 3
⊢ (𝜑 → (𝐶 ↾cat 𝐻) = ((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉)) |
102 | 101 | oveq1d 6564 |
. 2
⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (((𝐶 ↾s 𝑆) sSet 〈(Hom ‘ndx), 𝐻〉) ↾cat
𝐽)) |
103 | | eqid 2610 |
. . 3
⊢ (𝐶 ↾cat 𝐽) = (𝐶 ↾cat 𝐽) |
104 | 103, 100,
6, 7 | rescval2 16311 |
. 2
⊢ (𝜑 → (𝐶 ↾cat 𝐽) = ((𝐶 ↾s 𝑇) sSet 〈(Hom ‘ndx), 𝐽〉)) |
105 | 98, 102, 104 | 3eqtr4d 2654 |
1
⊢ (𝜑 → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) |