Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’ (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎcat π½) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)
βΎcat π½) |
2 | | ovexd 7397 |
. . . 4
β’ (π β ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) β
V) |
3 | | rescabs.s |
. . . . 5
β’ (π β π β π) |
4 | | rescabs.t |
. . . . 5
β’ (π β π β π) |
5 | 3, 4 | ssexd 5286 |
. . . 4
β’ (π β π β V) |
6 | | rescabs.j |
. . . 4
β’ (π β π½ Fn (π Γ π)) |
7 | 1, 2, 5, 6 | rescval2 17718 |
. . 3
β’ (π β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎcat
π½) = ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
8 | | simpr 486 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (Baseβ(πΆ βΎs π)) β π) |
9 | | ovexd 7397 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) β
V) |
10 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π β V) |
11 | | eqid 2737 |
. . . . . . . 8
β’ (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎs π) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)
βΎs π) |
12 | | baseid 17093 |
. . . . . . . . 9
β’ Base =
Slot (Baseβndx) |
13 | | slotsbhcdif 17303 |
. . . . . . . . . 10
β’
((Baseβndx) β (Hom βndx) β§ (Baseβndx) β
(compβndx) β§ (Hom βndx) β (compβndx)) |
14 | 13 | simp1i 1140 |
. . . . . . . . 9
β’
(Baseβndx) β (Hom βndx) |
15 | 12, 14 | setsnid 17088 |
. . . . . . . 8
β’
(Baseβ(πΆ
βΎs π)) =
(Baseβ((πΆ
βΎs π) sSet
β¨(Hom βndx), π»β©)) |
16 | 11, 15 | ressid2 17123 |
. . . . . . 7
β’
(((Baseβ(πΆ
βΎs π))
β π β§ ((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) β V β§
π β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎs π) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)) |
17 | 8, 9, 10, 16 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) = ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©)) |
18 | 17 | oveq1d 7377 |
. . . . 5
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©) sSet
β¨(Hom βndx), π½β©)) |
19 | | ovex 7395 |
. . . . . 6
β’ (πΆ βΎs π) β V |
20 | 5, 5 | xpexd 7690 |
. . . . . . . 8
β’ (π β (π Γ π) β V) |
21 | 6, 20 | fnexd 7173 |
. . . . . . 7
β’ (π β π½ β V) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π½ β V) |
23 | | setsabs 17058 |
. . . . . 6
β’ (((πΆ βΎs π) β V β§ π½ β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
24 | 19, 22, 23 | sylancr 588 |
. . . . 5
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
25 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (πΆ βΎs π) = (πΆ βΎs π) |
26 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(BaseβπΆ) =
(BaseβπΆ) |
27 | 25, 26 | ressbas 17125 |
. . . . . . . . . . . . 13
β’ (π β π β (π β© (BaseβπΆ)) = (Baseβ(πΆ βΎs π))) |
28 | 3, 27 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β© (BaseβπΆ)) = (Baseβ(πΆ βΎs π))) |
29 | 28 | sseq1d 3980 |
. . . . . . . . . . 11
β’ (π β ((π β© (BaseβπΆ)) β π β (Baseβ(πΆ βΎs π)) β π)) |
30 | 29 | biimpar 479 |
. . . . . . . . . 10
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β π) |
31 | | inss2 4194 |
. . . . . . . . . . 11
β’ (π β© (BaseβπΆ)) β (BaseβπΆ) |
32 | 31 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β (BaseβπΆ)) |
33 | 30, 32 | ssind 4197 |
. . . . . . . . 9
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β (π β© (BaseβπΆ))) |
34 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π β π) |
35 | 34 | ssrind 4200 |
. . . . . . . . 9
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β (π β© (BaseβπΆ))) |
36 | 33, 35 | eqssd 3966 |
. . . . . . . 8
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) = (π β© (BaseβπΆ))) |
37 | 36 | oveq2d 7378 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs (π β© (BaseβπΆ))) = (πΆ βΎs (π β© (BaseβπΆ)))) |
38 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π β π) |
39 | 26 | ressinbas 17133 |
. . . . . . . 8
β’ (π β π β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
40 | 38, 39 | syl 17 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
41 | 26 | ressinbas 17133 |
. . . . . . . 8
β’ (π β V β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
42 | 10, 41 | syl 17 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
43 | 37, 40, 42 | 3eqtr4d 2787 |
. . . . . 6
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) = (πΆ βΎs π)) |
44 | 43 | oveq1d 7377 |
. . . . 5
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©) = ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©)) |
45 | 18, 24, 44 | 3eqtrd 2781 |
. . . 4
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
46 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β Β¬ (Baseβ(πΆ βΎs π)) β π) |
47 | | ovexd 7397 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) β
V) |
48 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π β V) |
49 | 11, 15 | ressval2 17124 |
. . . . . . . 8
β’ ((Β¬
(Baseβ(πΆ
βΎs π))
β π β§ ((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) β V β§
π β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎs π) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©) sSet
β¨(Baseβndx), (π
β© (Baseβ(πΆ
βΎs π)))β©)) |
50 | 46, 47, 48, 49 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) = (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet
β¨(Baseβndx), (π
β© (Baseβ(πΆ
βΎs π)))β©)) |
51 | | ovexd 7397 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) β V) |
52 | 14 | necomi 2999 |
. . . . . . . . 9
β’ (Hom
βndx) β (Baseβndx) |
53 | 52 | a1i 11 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (Hom βndx) β
(Baseβndx)) |
54 | | rescabs.h |
. . . . . . . . . 10
β’ (π β π» Fn (π Γ π)) |
55 | 3, 3 | xpexd 7690 |
. . . . . . . . . 10
β’ (π β (π Γ π) β V) |
56 | 54, 55 | fnexd 7173 |
. . . . . . . . 9
β’ (π β π» β V) |
57 | 56 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π» β V) |
58 | | fvex 6860 |
. . . . . . . . . 10
β’
(Baseβ(πΆ
βΎs π))
β V |
59 | 58 | inex2 5280 |
. . . . . . . . 9
β’ (π β© (Baseβ(πΆ βΎs π))) β V |
60 | 59 | a1i 11 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (π β© (Baseβ(πΆ βΎs π))) β V) |
61 | | fvex 6860 |
. . . . . . . . 9
β’ (Hom
βndx) β V |
62 | | fvex 6860 |
. . . . . . . . 9
β’
(Baseβndx) β V |
63 | 61, 62 | setscom 17059 |
. . . . . . . 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), π»β©)) |
64 | 51, 53, 57, 60, 63 | syl22anc 838 |
. . . . . . 7
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet
β¨(Baseβndx), (π
β© (Baseβ(πΆ
βΎs π)))β©) = (((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©) sSet β¨(Hom
βndx), π»β©)) |
65 | | eqid 2737 |
. . . . . . . . . . 11
β’ ((πΆ βΎs π) βΎs π) = ((πΆ βΎs π) βΎs π) |
66 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβ(πΆ
βΎs π)) =
(Baseβ(πΆ
βΎs π)) |
67 | 65, 66 | ressval2 17124 |
. . . . . . . . . 10
β’ ((Β¬
(Baseβ(πΆ
βΎs π))
β π β§ (πΆ βΎs π) β V β§ π β V) β ((πΆ βΎs π) βΎs π) = ((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©)) |
68 | 46, 51, 48, 67 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) βΎs π) = ((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©)) |
69 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π β π) |
70 | | ressabs 17137 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πΆ βΎs π) βΎs π) = (πΆ βΎs π)) |
71 | 3, 69, 70 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) βΎs π) = (πΆ βΎs π)) |
72 | 68, 71 | eqtr3d 2779 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©) = (πΆ βΎs π)) |
73 | 72 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©) sSet β¨(Hom
βndx), π»β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)) |
74 | 50, 64, 73 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) = ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©)) |
75 | 74 | oveq1d 7377 |
. . . . 5
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©) sSet
β¨(Hom βndx), π½β©)) |
76 | | ovex 7395 |
. . . . . 6
β’ (πΆ βΎs π) β V |
77 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π½ β V) |
78 | | setsabs 17058 |
. . . . . 6
β’ (((πΆ βΎs π) β V β§ π½ β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
79 | 76, 77, 78 | sylancr 588 |
. . . . 5
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
80 | 75, 79 | eqtrd 2777 |
. . . 4
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
81 | 45, 80 | pm2.61dan 812 |
. . 3
β’ (π β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
82 | 7, 81 | eqtrd 2777 |
. 2
β’ (π β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎcat
π½) = ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©)) |
83 | | eqid 2737 |
. . . 4
β’ (πΆ βΎcat π») = (πΆ βΎcat π») |
84 | | rescabs.c |
. . . 4
β’ (π β πΆ β π) |
85 | 83, 84, 3, 54 | rescval2 17718 |
. . 3
β’ (π β (πΆ βΎcat π») = ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©)) |
86 | 85 | oveq1d 7377 |
. 2
β’ (π β ((πΆ βΎcat π») βΎcat π½) = (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎcat
π½)) |
87 | | eqid 2737 |
. . 3
β’ (πΆ βΎcat π½) = (πΆ βΎcat π½) |
88 | 87, 84, 5, 6 | rescval2 17718 |
. 2
β’ (π β (πΆ βΎcat π½) = ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©)) |
89 | 82, 86, 88 | 3eqtr4d 2787 |
1
β’ (π β ((πΆ βΎcat π») βΎcat π½) = (πΆ βΎcat π½)) |