Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . 7
β’ (π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) = (π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) |
2 | 1 | mptpreima 6195 |
. . . . . 6
β’ (β‘(π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) β π) = {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} |
3 | | tmdgsum2.1 |
. . . . . . . 8
β’ (π β πΊ β CMnd) |
4 | | tmdgsum2.2 |
. . . . . . . 8
β’ (π β πΊ β TopMnd) |
5 | | tmdgsum2.a |
. . . . . . . 8
β’ (π β π΄ β Fin) |
6 | | tmdgsum.j |
. . . . . . . . 9
β’ π½ = (TopOpenβπΊ) |
7 | | tmdgsum.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΊ) |
8 | 6, 7 | tmdgsum 23462 |
. . . . . . . 8
β’ ((πΊ β CMnd β§ πΊ β TopMnd β§ π΄ β Fin) β (π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) β ((π½ βko π« π΄) Cn π½)) |
9 | 3, 4, 5, 8 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) β ((π½ βko π« π΄) Cn π½)) |
10 | | tmdgsum2.u |
. . . . . . 7
β’ (π β π β π½) |
11 | | cnima 22632 |
. . . . . . 7
β’ (((π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) β ((π½ βko π« π΄) Cn π½) β§ π β π½) β (β‘(π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) β π) β (π½ βko π« π΄)) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . 6
β’ (π β (β‘(π β (π΅ βm π΄) β¦ (πΊ Ξ£g π)) β π) β (π½ βko π« π΄)) |
13 | 2, 12 | eqeltrrid 2843 |
. . . . 5
β’ (π β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β (π½ βko π« π΄)) |
14 | 6, 7 | tmdtopon 23448 |
. . . . . . . 8
β’ (πΊ β TopMnd β π½ β (TopOnβπ΅)) |
15 | | topontop 22278 |
. . . . . . . 8
β’ (π½ β (TopOnβπ΅) β π½ β Top) |
16 | 4, 14, 15 | 3syl 18 |
. . . . . . 7
β’ (π β π½ β Top) |
17 | | xkopt 23022 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β Fin) β (π½ βko π«
π΄) =
(βtβ(π΄ Γ {π½}))) |
18 | 16, 5, 17 | syl2anc 585 |
. . . . . 6
β’ (π β (π½ βko π« π΄) =
(βtβ(π΄ Γ {π½}))) |
19 | | fnconstg 6735 |
. . . . . . . 8
β’ (π½ β (TopOnβπ΅) β (π΄ Γ {π½}) Fn π΄) |
20 | 4, 14, 19 | 3syl 18 |
. . . . . . 7
β’ (π β (π΄ Γ {π½}) Fn π΄) |
21 | | eqid 2737 |
. . . . . . . 8
β’ {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} |
22 | 21 | ptval 22937 |
. . . . . . 7
β’ ((π΄ β Fin β§ (π΄ Γ {π½}) Fn π΄) β (βtβ(π΄ Γ {π½})) = (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))})) |
23 | 5, 20, 22 | syl2anc 585 |
. . . . . 6
β’ (π β
(βtβ(π΄ Γ {π½})) = (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))})) |
24 | 18, 23 | eqtrd 2777 |
. . . . 5
β’ (π β (π½ βko π« π΄) = (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))})) |
25 | 13, 24 | eleqtrd 2840 |
. . . 4
β’ (π β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))})) |
26 | | oveq2 7370 |
. . . . . 6
β’ (π = (π΄ Γ {π}) β (πΊ Ξ£g π) = (πΊ Ξ£g (π΄ Γ {π}))) |
27 | 26 | eleq1d 2823 |
. . . . 5
β’ (π = (π΄ Γ {π}) β ((πΊ Ξ£g π) β π β (πΊ Ξ£g (π΄ Γ {π})) β π)) |
28 | | tmdgsum2.x |
. . . . . . 7
β’ (π β π β π΅) |
29 | | fconst6g 6736 |
. . . . . . 7
β’ (π β π΅ β (π΄ Γ {π}):π΄βΆπ΅) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’ (π β (π΄ Γ {π}):π΄βΆπ΅) |
31 | 7 | fvexi 6861 |
. . . . . . 7
β’ π΅ β V |
32 | | elmapg 8785 |
. . . . . . 7
β’ ((π΅ β V β§ π΄ β Fin) β ((π΄ Γ {π}) β (π΅ βm π΄) β (π΄ Γ {π}):π΄βΆπ΅)) |
33 | 31, 5, 32 | sylancr 588 |
. . . . . 6
β’ (π β ((π΄ Γ {π}) β (π΅ βm π΄) β (π΄ Γ {π}):π΄βΆπ΅)) |
34 | 30, 33 | mpbird 257 |
. . . . 5
β’ (π β (π΄ Γ {π}) β (π΅ βm π΄)) |
35 | | fconstmpt 5699 |
. . . . . . . 8
β’ (π΄ Γ {π}) = (π β π΄ β¦ π) |
36 | 35 | oveq2i 7373 |
. . . . . . 7
β’ (πΊ Ξ£g
(π΄ Γ {π})) = (πΊ Ξ£g (π β π΄ β¦ π)) |
37 | | cmnmnd 19586 |
. . . . . . . . 9
β’ (πΊ β CMnd β πΊ β Mnd) |
38 | 3, 37 | syl 17 |
. . . . . . . 8
β’ (π β πΊ β Mnd) |
39 | | tmdgsum2.t |
. . . . . . . . 9
β’ Β· =
(.gβπΊ) |
40 | 7, 39 | gsumconst 19718 |
. . . . . . . 8
β’ ((πΊ β Mnd β§ π΄ β Fin β§ π β π΅) β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) |
41 | 38, 5, 28, 40 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((β―βπ΄) Β· π)) |
42 | 36, 41 | eqtrid 2789 |
. . . . . 6
β’ (π β (πΊ Ξ£g (π΄ Γ {π})) = ((β―βπ΄) Β· π)) |
43 | | tmdgsum2.3 |
. . . . . 6
β’ (π β ((β―βπ΄) Β· π) β π) |
44 | 42, 43 | eqeltrd 2838 |
. . . . 5
β’ (π β (πΊ Ξ£g (π΄ Γ {π})) β π) |
45 | 27, 34, 44 | elrabd 3652 |
. . . 4
β’ (π β (π΄ Γ {π}) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) |
46 | | tg2 22331 |
. . . 4
β’ (({π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))}) β§ (π΄ Γ {π}) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ‘ β {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} ((π΄ Γ {π}) β π‘ β§ π‘ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) |
47 | 25, 45, 46 | syl2anc 585 |
. . 3
β’ (π β βπ‘ β {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} ((π΄ Γ {π}) β π‘ β§ π‘ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) |
48 | | eleq2 2827 |
. . . . 5
β’ (π‘ = π₯ β ((π΄ Γ {π}) β π‘ β (π΄ Γ {π}) β π₯)) |
49 | | sseq1 3974 |
. . . . 5
β’ (π‘ = π₯ β (π‘ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) |
50 | 48, 49 | anbi12d 632 |
. . . 4
β’ (π‘ = π₯ β (((π΄ Γ {π}) β π‘ β§ π‘ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β ((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}))) |
51 | 50 | rexab2 3662 |
. . 3
β’
(βπ‘ β
{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} ((π΄ Γ {π}) β π‘ β§ π‘ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ₯(βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)) β§ ((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}))) |
52 | 47, 51 | sylib 217 |
. 2
β’ (π β βπ₯(βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)) β§ ((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}))) |
53 | | toponuni 22279 |
. . . . . . . . . . . . . 14
β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) |
54 | 4, 14, 53 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β π΅ = βͺ π½) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π΅ = βͺ π½) |
56 | 55 | ineq1d 4176 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (π΅ β© β© ran
π) = (βͺ π½
β© β© ran π)) |
57 | 16 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π½ β Top) |
58 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π Fn π΄) |
59 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦)) |
60 | | fvconst2g 7156 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β Top β§ π¦ β π΄) β ((π΄ Γ {π½})βπ¦) = π½) |
61 | 60 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π¦ β π΄) β ((πβπ¦) β ((π΄ Γ {π½})βπ¦) β (πβπ¦) β π½)) |
62 | 61 | ralbidva 3173 |
. . . . . . . . . . . . . . . 16
β’ (π½ β Top β
(βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β βπ¦ β π΄ (πβπ¦) β π½)) |
63 | 57, 62 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β βπ¦ β π΄ (πβπ¦) β π½)) |
64 | 59, 63 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ¦ β π΄ (πβπ¦) β π½) |
65 | | ffnfv 7071 |
. . . . . . . . . . . . . 14
β’ (π:π΄βΆπ½ β (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β π½)) |
66 | 58, 64, 65 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π:π΄βΆπ½) |
67 | 66 | frnd 6681 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β ran π β π½) |
68 | 5 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π΄ β Fin) |
69 | | dffn4 6767 |
. . . . . . . . . . . . . 14
β’ (π Fn π΄ β π:π΄βontoβran π) |
70 | 58, 69 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π:π΄βontoβran π) |
71 | | fofi 9289 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π:π΄βontoβran π) β ran π β Fin) |
72 | 68, 70, 71 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β ran π β Fin) |
73 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
74 | 73 | rintopn 22274 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ ran π β π½ β§ ran π β Fin) β (βͺ π½
β© β© ran π) β π½) |
75 | 57, 67, 72, 74 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (βͺ
π½ β© β© ran π) β π½) |
76 | 56, 75 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (π΅ β© β© ran
π) β π½) |
77 | 28 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π β π΅) |
78 | | fconstmpt 5699 |
. . . . . . . . . . . . . 14
β’ (π΄ Γ {π}) = (π¦ β π΄ β¦ π) |
79 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦)) |
80 | 78, 79 | eqeltrrid 2843 |
. . . . . . . . . . . . 13
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (π¦ β π΄ β¦ π) β Xπ¦ β π΄ (πβπ¦)) |
81 | | mptelixpg 8880 |
. . . . . . . . . . . . . 14
β’ (π΄ β Fin β ((π¦ β π΄ β¦ π) β Xπ¦ β π΄ (πβπ¦) β βπ¦ β π΄ π β (πβπ¦))) |
82 | 68, 81 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β ((π¦ β π΄ β¦ π) β Xπ¦ β π΄ (πβπ¦) β βπ¦ β π΄ π β (πβπ¦))) |
83 | 80, 82 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ¦ β π΄ π β (πβπ¦)) |
84 | | eleq2 2827 |
. . . . . . . . . . . . . 14
β’ (π§ = (πβπ¦) β (π β π§ β π β (πβπ¦))) |
85 | 84 | ralrn 7043 |
. . . . . . . . . . . . 13
β’ (π Fn π΄ β (βπ§ β ran π π β π§ β βπ¦ β π΄ π β (πβπ¦))) |
86 | 58, 85 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β (βπ§ β ran π π β π§ β βπ¦ β π΄ π β (πβπ¦))) |
87 | 83, 86 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ§ β ran π π β π§) |
88 | | elrint 4957 |
. . . . . . . . . . 11
β’ (π β (π΅ β© β© ran
π) β (π β π΅ β§ βπ§ β ran π π β π§)) |
89 | 77, 87, 88 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β π β (π΅ β© β© ran
π)) |
90 | 31 | inex1 5279 |
. . . . . . . . . . . . 13
β’ (π΅ β© β© ran π) β V |
91 | | ixpconstg 8851 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ (π΅ β© β© ran π) β V) β Xπ¦ β
π΄ (π΅ β© β© ran
π) = ((π΅ β© β© ran
π) βm π΄)) |
92 | 68, 90, 91 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β Xπ¦ β π΄ (π΅ β© β© ran
π) = ((π΅ β© β© ran
π) βm π΄)) |
93 | | inss2 4194 |
. . . . . . . . . . . . . . 15
β’ (π΅ β© β© ran π) β β© ran
π |
94 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn π΄ β§ π¦ β π΄) β (πβπ¦) β ran π) |
95 | | intss1 4929 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ¦) β ran π β β© ran
π β (πβπ¦)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π Fn π΄ β§ π¦ β π΄) β β© ran
π β (πβπ¦)) |
97 | 93, 96 | sstrid 3960 |
. . . . . . . . . . . . . 14
β’ ((π Fn π΄ β§ π¦ β π΄) β (π΅ β© β© ran
π) β (πβπ¦)) |
98 | 97 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (π Fn π΄ β βπ¦ β π΄ (π΅ β© β© ran
π) β (πβπ¦)) |
99 | | ss2ixp 8855 |
. . . . . . . . . . . . 13
β’
(βπ¦ β
π΄ (π΅ β© β© ran
π) β (πβπ¦) β Xπ¦ β π΄ (π΅ β© β© ran
π) β Xπ¦ β
π΄ (πβπ¦)) |
100 | 58, 98, 99 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β Xπ¦ β π΄ (π΅ β© β© ran
π) β Xπ¦ β
π΄ (πβπ¦)) |
101 | 92, 100 | eqsstrrd 3988 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β ((π΅ β© β© ran
π) βm π΄) β Xπ¦ β
π΄ (πβπ¦)) |
102 | | ssrab 4035 |
. . . . . . . . . . . . 13
β’ (Xπ¦ β
π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β (Xπ¦ β π΄ (πβπ¦) β (π΅ βm π΄) β§ βπ β X π¦ β π΄ (πβπ¦)(πΊ Ξ£g π) β π)) |
103 | 102 | simprbi 498 |
. . . . . . . . . . . 12
β’ (Xπ¦ β
π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β βπ β X π¦ β π΄ (πβπ¦)(πΊ Ξ£g π) β π) |
104 | 103 | ad2antll 728 |
. . . . . . . . . . 11
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ β X π¦ β π΄ (πβπ¦)(πΊ Ξ£g π) β π) |
105 | | ssralv 4015 |
. . . . . . . . . . 11
β’ (((π΅ β© β© ran π) βm π΄) β Xπ¦ β π΄ (πβπ¦) β (βπ β X π¦ β π΄ (πβπ¦)(πΊ Ξ£g π) β π β βπ β ((π΅ β© β© ran
π) βm π΄)(πΊ Ξ£g π) β π)) |
106 | 101, 104,
105 | sylc 65 |
. . . . . . . . . 10
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ β ((π΅ β© β© ran
π) βm π΄)(πΊ Ξ£g π) β π) |
107 | | eleq2 2827 |
. . . . . . . . . . . 12
β’ (π’ = (π΅ β© β© ran
π) β (π β π’ β π β (π΅ β© β© ran
π))) |
108 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π’ = (π΅ β© β© ran
π) β (π’ βm π΄) = ((π΅ β© β© ran
π) βm π΄)) |
109 | 108 | raleqdv 3316 |
. . . . . . . . . . . 12
β’ (π’ = (π΅ β© β© ran
π) β (βπ β (π’ βm π΄)(πΊ Ξ£g π) β π β βπ β ((π΅ β© β© ran
π) βm π΄)(πΊ Ξ£g π) β π)) |
110 | 107, 109 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π’ = (π΅ β© β© ran
π) β ((π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π) β (π β (π΅ β© β© ran
π) β§ βπ β ((π΅ β© β© ran
π) βm π΄)(πΊ Ξ£g π) β π))) |
111 | 110 | rspcev 3584 |
. . . . . . . . . 10
β’ (((π΅ β© β© ran π) β π½ β§ (π β (π΅ β© β© ran
π) β§ βπ β ((π΅ β© β© ran
π) βm π΄)(πΊ Ξ£g π) β π)) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)) |
112 | 76, 89, 106, 111 | syl12anc 836 |
. . . . . . . . 9
β’ (((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β§ ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)) |
113 | 112 | ex 414 |
. . . . . . . 8
β’ ((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦))) β (((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π))) |
114 | 113 | 3adantr3 1172 |
. . . . . . 7
β’ ((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦))) β (((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π))) |
115 | | eleq2 2827 |
. . . . . . . . 9
β’ (π₯ = Xπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π}) β π₯ β (π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦))) |
116 | | sseq1 3974 |
. . . . . . . . 9
β’ (π₯ = Xπ¦ β π΄ (πβπ¦) β (π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π} β Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) |
117 | 115, 116 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = Xπ¦ β π΄ (πβπ¦) β (((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β ((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}))) |
118 | 117 | imbi1d 342 |
. . . . . . 7
β’ (π₯ = Xπ¦ β π΄ (πβπ¦) β ((((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)) β (((π΄ Γ {π}) β Xπ¦ β π΄ (πβπ¦) β§ Xπ¦ β π΄ (πβπ¦) β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)))) |
119 | 114, 118 | syl5ibrcom 247 |
. . . . . 6
β’ ((π β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦))) β (π₯ = Xπ¦ β π΄ (πβπ¦) β (((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)))) |
120 | 119 | expimpd 455 |
. . . . 5
β’ (π β (((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)) β (((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)))) |
121 | 120 | exlimdv 1937 |
. . . 4
β’ (π β (βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)) β (((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π}) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)))) |
122 | 121 | impd 412 |
. . 3
β’ (π β ((βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)) β§ ((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π))) |
123 | 122 | exlimdv 1937 |
. 2
β’ (π β (βπ₯(βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β ((π΄ Γ {π½})βπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ ((π΄ Γ {π½})βπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)) β§ ((π΄ Γ {π}) β π₯ β§ π₯ β {π β (π΅ βm π΄) β£ (πΊ Ξ£g π) β π})) β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π))) |
124 | 52, 123 | mpd 15 |
1
β’ (π β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)) |