Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . . 4
β’ (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎcat π½) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)
βΎcat π½) |
2 | | ovexd 7446 |
. . . 4
β’ (π β ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) β
V) |
3 | | rescabs.s |
. . . . 5
β’ (π β π β π) |
4 | | rescabs.t |
. . . . 5
β’ (π β π β π) |
5 | 3, 4 | ssexd 5324 |
. . . 4
β’ (π β π β V) |
6 | | rescabs.j |
. . . 4
β’ (π β π½ Fn (π Γ π)) |
7 | 1, 2, 5, 6 | rescval2 17777 |
. . 3
β’ (π β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎcat
π½) = ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
8 | | simpr 485 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (Baseβ(πΆ βΎs π)) β π) |
9 | | ovexd 7446 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) β
V) |
10 | 5 | adantr 481 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π β V) |
11 | | eqid 2732 |
. . . . . . . 8
β’ (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎs π) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)
βΎs π) |
12 | | baseid 17149 |
. . . . . . . . 9
β’ Base =
Slot (Baseβndx) |
13 | | 1re 11216 |
. . . . . . . . . . 11
β’ 1 β
β |
14 | | 1nn 12225 |
. . . . . . . . . . . 12
β’ 1 β
β |
15 | | 4nn0 12493 |
. . . . . . . . . . . 12
β’ 4 β
β0 |
16 | | 1nn0 12490 |
. . . . . . . . . . . 12
β’ 1 β
β0 |
17 | | 1lt10 12818 |
. . . . . . . . . . . 12
β’ 1 <
;10 |
18 | 14, 15, 16, 17 | declti 12717 |
. . . . . . . . . . 11
β’ 1 <
;14 |
19 | 13, 18 | ltneii 11329 |
. . . . . . . . . 10
β’ 1 β
;14 |
20 | | basendx 17155 |
. . . . . . . . . . 11
β’
(Baseβndx) = 1 |
21 | | homndx 17358 |
. . . . . . . . . . 11
β’ (Hom
βndx) = ;14 |
22 | 20, 21 | neeq12i 3007 |
. . . . . . . . . 10
β’
((Baseβndx) β (Hom βndx) β 1 β ;14) |
23 | 19, 22 | mpbir 230 |
. . . . . . . . 9
β’
(Baseβndx) β (Hom βndx) |
24 | 12, 23 | setsnid 17144 |
. . . . . . . 8
β’
(Baseβ(πΆ
βΎs π)) =
(Baseβ((πΆ
βΎs π) sSet
β¨(Hom βndx), π»β©)) |
25 | 11, 24 | ressid2 17179 |
. . . . . . 7
β’
(((Baseβ(πΆ
βΎs π))
β π β§ ((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) β V β§
π β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎs π) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)) |
26 | 8, 9, 10, 25 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) = ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©)) |
27 | 26 | oveq1d 7426 |
. . . . 5
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©) sSet
β¨(Hom βndx), π½β©)) |
28 | | ovex 7444 |
. . . . . 6
β’ (πΆ βΎs π) β V |
29 | 5, 5 | xpexd 7740 |
. . . . . . . 8
β’ (π β (π Γ π) β V) |
30 | | fnex 7221 |
. . . . . . . 8
β’ ((π½ Fn (π Γ π) β§ (π Γ π) β V) β π½ β V) |
31 | 6, 29, 30 | syl2anc 584 |
. . . . . . 7
β’ (π β π½ β V) |
32 | 31 | adantr 481 |
. . . . . 6
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π½ β V) |
33 | | setsabs 17114 |
. . . . . 6
β’ (((πΆ βΎs π) β V β§ π½ β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
34 | 28, 32, 33 | sylancr 587 |
. . . . 5
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
35 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ (πΆ βΎs π) = (πΆ βΎs π) |
36 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(BaseβπΆ) =
(BaseβπΆ) |
37 | 35, 36 | ressbas 17181 |
. . . . . . . . . . . . 13
β’ (π β π β (π β© (BaseβπΆ)) = (Baseβ(πΆ βΎs π))) |
38 | 3, 37 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β© (BaseβπΆ)) = (Baseβ(πΆ βΎs π))) |
39 | 38 | sseq1d 4013 |
. . . . . . . . . . 11
β’ (π β ((π β© (BaseβπΆ)) β π β (Baseβ(πΆ βΎs π)) β π)) |
40 | 39 | biimpar 478 |
. . . . . . . . . 10
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β π) |
41 | | inss2 4229 |
. . . . . . . . . . 11
β’ (π β© (BaseβπΆ)) β (BaseβπΆ) |
42 | 41 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β (BaseβπΆ)) |
43 | 40, 42 | ssind 4232 |
. . . . . . . . 9
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β (π β© (BaseβπΆ))) |
44 | 4 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π β π) |
45 | 44 | ssrind 4235 |
. . . . . . . . 9
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) β (π β© (BaseβπΆ))) |
46 | 43, 45 | eqssd 3999 |
. . . . . . . 8
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (π β© (BaseβπΆ)) = (π β© (BaseβπΆ))) |
47 | 46 | oveq2d 7427 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs (π β© (BaseβπΆ))) = (πΆ βΎs (π β© (BaseβπΆ)))) |
48 | 3 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β π β π) |
49 | 36 | ressinbas 17192 |
. . . . . . . 8
β’ (π β π β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
50 | 48, 49 | syl 17 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
51 | 36 | ressinbas 17192 |
. . . . . . . 8
β’ (π β V β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
52 | 10, 51 | syl 17 |
. . . . . . 7
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
53 | 47, 50, 52 | 3eqtr4d 2782 |
. . . . . 6
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) = (πΆ βΎs π)) |
54 | 53 | oveq1d 7426 |
. . . . 5
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©) = ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©)) |
55 | 27, 34, 54 | 3eqtrd 2776 |
. . . 4
β’ ((π β§ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
56 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β Β¬ (Baseβ(πΆ βΎs π)) β π) |
57 | | ovexd 7446 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) β
V) |
58 | 5 | adantr 481 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π β V) |
59 | 11, 24 | ressval2 17180 |
. . . . . . . 8
β’ ((Β¬
(Baseβ(πΆ
βΎs π))
β π β§ ((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) β V β§
π β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©)
βΎs π) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©) sSet
β¨(Baseβndx), (π
β© (Baseβ(πΆ
βΎs π)))β©)) |
60 | 56, 57, 58, 59 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) = (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet
β¨(Baseβndx), (π
β© (Baseβ(πΆ
βΎs π)))β©)) |
61 | | ovexd 7446 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (πΆ βΎs π) β V) |
62 | 23 | necomi 2995 |
. . . . . . . . 9
β’ (Hom
βndx) β (Baseβndx) |
63 | 62 | a1i 11 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (Hom βndx) β
(Baseβndx)) |
64 | | rescabs.h |
. . . . . . . . . 10
β’ (π β π» Fn (π Γ π)) |
65 | 3, 3 | xpexd 7740 |
. . . . . . . . . 10
β’ (π β (π Γ π) β V) |
66 | | fnex 7221 |
. . . . . . . . . 10
β’ ((π» Fn (π Γ π) β§ (π Γ π) β V) β π» β V) |
67 | 64, 65, 66 | syl2anc 584 |
. . . . . . . . 9
β’ (π β π» β V) |
68 | 67 | adantr 481 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π» β V) |
69 | | fvex 6904 |
. . . . . . . . . 10
β’
(Baseβ(πΆ
βΎs π))
β V |
70 | 69 | inex2 5318 |
. . . . . . . . 9
β’ (π β© (Baseβ(πΆ βΎs π))) β V |
71 | 70 | a1i 11 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (π β© (Baseβ(πΆ βΎs π))) β V) |
72 | | fvex 6904 |
. . . . . . . . 9
β’ (Hom
βndx) β V |
73 | | fvex 6904 |
. . . . . . . . 9
β’
(Baseβndx) β V |
74 | 72, 73 | setscom 17115 |
. . . . . . . 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), π»β©)) |
75 | 61, 63, 68, 71, 74 | syl22anc 837 |
. . . . . . 7
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet
β¨(Baseβndx), (π
β© (Baseβ(πΆ
βΎs π)))β©) = (((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©) sSet β¨(Hom
βndx), π»β©)) |
76 | | eqid 2732 |
. . . . . . . . . . 11
β’ ((πΆ βΎs π) βΎs π) = ((πΆ βΎs π) βΎs π) |
77 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβ(πΆ
βΎs π)) =
(Baseβ(πΆ
βΎs π)) |
78 | 76, 77 | ressval2 17180 |
. . . . . . . . . 10
β’ ((Β¬
(Baseβ(πΆ
βΎs π))
β π β§ (πΆ βΎs π) β V β§ π β V) β ((πΆ βΎs π) βΎs π) = ((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©)) |
79 | 56, 61, 58, 78 | syl3anc 1371 |
. . . . . . . . 9
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) βΎs π) = ((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©)) |
80 | 3 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π β π) |
81 | 4 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π β π) |
82 | | ressabs 17196 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πΆ βΎs π) βΎs π) = (πΆ βΎs π)) |
83 | 80, 81, 82 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) βΎs π) = (πΆ βΎs π)) |
84 | 79, 83 | eqtr3d 2774 |
. . . . . . . 8
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©) = (πΆ βΎs π)) |
85 | 84 | oveq1d 7426 |
. . . . . . 7
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Baseβndx), (π β© (Baseβ(πΆ βΎs π)))β©) sSet β¨(Hom
βndx), π»β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©)) |
86 | 60, 75, 85 | 3eqtrd 2776 |
. . . . . 6
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) = ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©)) |
87 | 86 | oveq1d 7426 |
. . . . 5
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
(((πΆ βΎs
π) sSet β¨(Hom
βndx), π»β©) sSet
β¨(Hom βndx), π½β©)) |
88 | | ovex 7444 |
. . . . . 6
β’ (πΆ βΎs π) β V |
89 | 31 | adantr 481 |
. . . . . 6
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β π½ β V) |
90 | | setsabs 17114 |
. . . . . 6
β’ (((πΆ βΎs π) β V β§ π½ β V) β (((πΆ βΎs π) sSet β¨(Hom βndx),
π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
91 | 88, 89, 90 | sylancr 587 |
. . . . 5
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
92 | 87, 91 | eqtrd 2772 |
. . . 4
β’ ((π β§ Β¬ (Baseβ(πΆ βΎs π)) β π) β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
93 | 55, 92 | pm2.61dan 811 |
. . 3
β’ (π β ((((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎs
π) sSet β¨(Hom
βndx), π½β©) =
((πΆ βΎs
π) sSet β¨(Hom
βndx), π½β©)) |
94 | 7, 93 | eqtrd 2772 |
. 2
β’ (π β (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎcat
π½) = ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©)) |
95 | | eqid 2732 |
. . . 4
β’ (πΆ βΎcat π») = (πΆ βΎcat π») |
96 | | rescabs.c |
. . . 4
β’ (π β πΆ β π) |
97 | 95, 96, 3, 64 | rescval2 17777 |
. . 3
β’ (π β (πΆ βΎcat π») = ((πΆ βΎs π) sSet β¨(Hom βndx), π»β©)) |
98 | 97 | oveq1d 7426 |
. 2
β’ (π β ((πΆ βΎcat π») βΎcat π½) = (((πΆ βΎs π) sSet β¨(Hom βndx), π»β©) βΎcat
π½)) |
99 | | eqid 2732 |
. . 3
β’ (πΆ βΎcat π½) = (πΆ βΎcat π½) |
100 | 99, 96, 5, 6 | rescval2 17777 |
. 2
β’ (π β (πΆ βΎcat π½) = ((πΆ βΎs π) sSet β¨(Hom βndx), π½β©)) |
101 | 94, 98, 100 | 3eqtr4d 2782 |
1
β’ (π β ((πΆ βΎcat π») βΎcat π½) = (πΆ βΎcat π½)) |