Step | Hyp | Ref
| Expression |
1 | | flimfcls 23393 |
. . . . 5
β’ (π½ fLim π) β (π½ fClus π) |
2 | | flimtop 23332 |
. . . . . . . . 9
β’ (π΄ β (π½ fLim πΉ) β π½ β Top) |
3 | | flimfnfcls.x |
. . . . . . . . . 10
β’ π = βͺ
π½ |
4 | 3 | toptopon 22282 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnβπ)) |
5 | 2, 4 | sylib 217 |
. . . . . . . 8
β’ (π΄ β (π½ fLim πΉ) β π½ β (TopOnβπ)) |
6 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β π½ β (TopOnβπ)) |
7 | | simplr 768 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β π β (Filβπ)) |
8 | | simpr 486 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β πΉ β π) |
9 | | flimss2 23339 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β (Filβπ) β§ πΉ β π) β (π½ fLim πΉ) β (π½ fLim π)) |
10 | 6, 7, 8, 9 | syl3anc 1372 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β (π½ fLim πΉ) β (π½ fLim π)) |
11 | | simpll 766 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β π΄ β (π½ fLim πΉ)) |
12 | 10, 11 | sseldd 3950 |
. . . . 5
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β π΄ β (π½ fLim π)) |
13 | 1, 12 | sselid 3947 |
. . . 4
β’ (((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β§ πΉ β π) β π΄ β (π½ fClus π)) |
14 | 13 | ex 414 |
. . 3
β’ ((π΄ β (π½ fLim πΉ) β§ π β (Filβπ)) β (πΉ β π β π΄ β (π½ fClus π))) |
15 | 14 | ralrimiva 3144 |
. 2
β’ (π΄ β (π½ fLim πΉ) β βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π))) |
16 | | sseq2 3975 |
. . . . . 6
β’ (π = πΉ β (πΉ β π β πΉ β πΉ)) |
17 | | oveq2 7370 |
. . . . . . 7
β’ (π = πΉ β (π½ fClus π) = (π½ fClus πΉ)) |
18 | 17 | eleq2d 2824 |
. . . . . 6
β’ (π = πΉ β (π΄ β (π½ fClus π) β π΄ β (π½ fClus πΉ))) |
19 | 16, 18 | imbi12d 345 |
. . . . 5
β’ (π = πΉ β ((πΉ β π β π΄ β (π½ fClus π)) β (πΉ β πΉ β π΄ β (π½ fClus πΉ)))) |
20 | 19 | rspcv 3580 |
. . . 4
β’ (πΉ β (Filβπ) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (πΉ β πΉ β π΄ β (π½ fClus πΉ)))) |
21 | | ssid 3971 |
. . . . . 6
β’ πΉ β πΉ |
22 | | id 22 |
. . . . . 6
β’ ((πΉ β πΉ β π΄ β (π½ fClus πΉ)) β (πΉ β πΉ β π΄ β (π½ fClus πΉ))) |
23 | 21, 22 | mpi 20 |
. . . . 5
β’ ((πΉ β πΉ β π΄ β (π½ fClus πΉ)) β π΄ β (π½ fClus πΉ)) |
24 | | fclstop 23378 |
. . . . . 6
β’ (π΄ β (π½ fClus πΉ) β π½ β Top) |
25 | 3 | fclselbas 23383 |
. . . . . 6
β’ (π΄ β (π½ fClus πΉ) β π΄ β π) |
26 | 24, 25 | jca 513 |
. . . . 5
β’ (π΄ β (π½ fClus πΉ) β (π½ β Top β§ π΄ β π)) |
27 | 23, 26 | syl 17 |
. . . 4
β’ ((πΉ β πΉ β π΄ β (π½ fClus πΉ)) β (π½ β Top β§ π΄ β π)) |
28 | 20, 27 | syl6 35 |
. . 3
β’ (πΉ β (Filβπ) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (π½ β Top β§ π΄ β π))) |
29 | | disjdif 4436 |
. . . . . . . . . . . . . 14
β’ (π β© (π β π)) = β
|
30 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β πΉ β (Filβπ)) |
31 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β π½ β Top) |
32 | 3 | topopn 22271 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π½ β Top β π β π½) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β π β π½) |
34 | | pwexg 5338 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π½ β π« π β V) |
35 | | rabexg 5293 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(π« π β
V β {π₯ β
π« π β£ (π β π) β π₯} β V) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β {π₯ β π« π β£ (π β π) β π₯} β V) |
37 | | unexg 7688 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ β (Filβπ) β§ {π₯ β π« π β£ (π β π) β π₯} β V) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β V) |
38 | 30, 36, 37 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β V) |
39 | | ssfii 9362 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β V β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β (fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β (fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) |
41 | | filsspw 23218 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ β (Filβπ) β πΉ β π« π) |
42 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ {π₯ β π« π β£ (π β π) β π₯} β π« π |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ β (Filβπ) β {π₯ β π« π β£ (π β π) β π₯} β π« π) |
44 | 41, 43 | unssd 4151 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΉ β (Filβπ) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β π« π) |
45 | 44 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β π« π) |
46 | | ssun2 4138 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ {π₯ β π« π β£ (π β π) β π₯} β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) |
47 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = (π β π) β ((π β π) β π₯ β (π β π) β (π β π))) |
48 | | difss 4096 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π) β π |
49 | | elpw2g 5306 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π½ β ((π β π) β π« π β (π β π) β π)) |
50 | 33, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β ((π β π) β π« π β (π β π) β π)) |
51 | 48, 50 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β π« π) |
52 | | ssid 3971 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π) β (π β π) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β (π β π)) |
54 | 47, 51, 53 | elrabd 3652 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β {π₯ β π« π β£ (π β π) β π₯}) |
55 | 46, 54 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) |
56 | 55 | ne0d 4300 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β β
) |
57 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ = π§ β ((π β π) β π₯ β (π β π) β π§)) |
58 | 57 | elrab 3650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ β {π₯ β π« π β£ (π β π) β π₯} β (π§ β π« π β§ (π β π) β π§)) |
59 | 58 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β {π₯ β π« π β£ (π β π) β π₯} β (π β π) β π§) |
60 | 59 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (π β π) β π§) |
61 | | sslin 4199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π) β π§ β (π¦ β© (π β π)) β (π¦ β© π§)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (π¦ β© (π β π)) β (π¦ β© π§)) |
63 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β Β¬ π β πΉ) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β Β¬ π β πΉ) |
65 | | inssdif0 4334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ β© π) β π β (π¦ β© (π β π)) = β
) |
66 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β πΉ β (Filβπ)) |
67 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β π¦ β πΉ) |
68 | | filelss 23219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΉ β (Filβπ) β§ π¦ β πΉ) β π¦ β π) |
69 | 66, 67, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β π¦ β π) |
70 | | df-ss 3932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π¦ β π β (π¦ β© π) = π¦) |
71 | 69, 70 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (π¦ β© π) = π¦) |
72 | 71 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β ((π¦ β© π) β π β π¦ β π)) |
73 | 30 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((πΉ β
(Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β§ π¦ β π) β πΉ β (Filβπ)) |
74 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((πΉ β
(Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β§ π¦ β π) β π¦ β πΉ) |
75 | | elssuni 4903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π½ β π β βͺ π½) |
76 | 75, 3 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β π½ β π β π) |
77 | 76 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β π β π) |
78 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((πΉ β
(Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β§ π¦ β π) β π β π) |
79 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((πΉ β
(Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β§ π¦ β π) β π¦ β π) |
80 | | filss 23220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΉ β (Filβπ) β§ (π¦ β πΉ β§ π β π β§ π¦ β π)) β π β πΉ) |
81 | 73, 74, 78, 79, 80 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((πΉ β
(Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β§ π¦ β π) β π β πΉ) |
82 | 81 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (π¦ β π β π β πΉ)) |
83 | 72, 82 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β ((π¦ β© π) β π β π β πΉ)) |
84 | 65, 83 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β ((π¦ β© (π β π)) = β
β π β πΉ)) |
85 | 84 | necon3bd 2958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (Β¬ π β πΉ β (π¦ β© (π β π)) β β
)) |
86 | 64, 85 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (π¦ β© (π β π)) β β
) |
87 | | ssn0 4365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β© (π β π)) β (π¦ β© π§) β§ (π¦ β© (π β π)) β β
) β (π¦ β© π§) β β
) |
88 | 62, 86, 87 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ (π¦ β πΉ β§ π§ β {π₯ β π« π β£ (π β π) β π₯})) β (π¦ β© π§) β β
) |
89 | 88 | ralrimivva 3198 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β βπ¦ β πΉ βπ§ β {π₯ β π« π β£ (π β π) β π₯} (π¦ β© π§) β β
) |
90 | | filfbas 23215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) |
91 | 30, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β πΉ β (fBasβπ)) |
92 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β π) |
93 | | filtop 23222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΉ β (Filβπ) β π β πΉ) |
94 | 30, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β π β πΉ) |
95 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (π β πΉ β π β πΉ)) |
96 | 94, 95 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π = π β π β πΉ)) |
97 | 96 | necon3bd 2958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (Β¬ π β πΉ β π β π)) |
98 | 63, 97 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β π β π) |
99 | | pssdifn0 4330 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π β§ π β π) β (π β π) β β
) |
100 | 77, 98, 99 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β β
) |
101 | | supfil 23262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π½ β§ (π β π) β π β§ (π β π) β β
) β {π₯ β π« π β£ (π β π) β π₯} β (Filβπ)) |
102 | 33, 92, 100, 101 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β {π₯ β π« π β£ (π β π) β π₯} β (Filβπ)) |
103 | | filfbas 23215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ({π₯ β π« π β£ (π β π) β π₯} β (Filβπ) β {π₯ β π« π β£ (π β π) β π₯} β (fBasβπ)) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β {π₯ β π« π β£ (π β π) β π₯} β (fBasβπ)) |
105 | | fbunfip 23236 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉ β (fBasβπ) β§ {π₯ β π« π β£ (π β π) β π₯} β (fBasβπ)) β (Β¬ β
β
(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β βπ¦ β πΉ βπ§ β {π₯ β π« π β£ (π β π) β π₯} (π¦ β© π§) β β
)) |
106 | 91, 104, 105 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (Β¬ β
β
(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β βπ¦ β πΉ βπ§ β {π₯ β π« π β£ (π β π) β π₯} (π¦ β© π§) β β
)) |
107 | 89, 106 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β Β¬ β
β
(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) |
108 | | fsubbas 23234 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΉ β ((fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β (fBasβπ) β ((πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β π« π β§ (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β β
β§ Β¬ β
β
(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) |
109 | 94, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β ((fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β (fBasβπ) β ((πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β π« π β§ (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β β
β§ Β¬ β
β
(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) |
110 | 45, 56, 107, 109 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β (fBasβπ)) |
111 | | ssfg 23239 |
. . . . . . . . . . . . . . . . . . . 20
β’
((fiβ(πΉ βͺ
{π₯ β π« π β£ (π β π) β π₯})) β (fBasβπ) β (fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) |
113 | 40, 112 | sstrd 3959 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) |
114 | 113 | unssad 4152 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β πΉ β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) |
115 | | fgcl 23245 |
. . . . . . . . . . . . . . . . . . 19
β’
((fiβ(πΉ βͺ
{π₯ β π« π β£ (π β π) β π₯})) β (fBasβπ) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β (Filβπ)) |
116 | 110, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β (Filβπ)) |
117 | | sseq2 3975 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β (πΉ β π β πΉ β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) |
118 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β (π½ fClus π) = (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) |
119 | 118 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β (π΄ β (π½ fClus π) β π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))))) |
120 | 117, 119 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β ((πΉ β π β π΄ β (π½ fClus π)) β (πΉ β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))))) |
121 | 120 | rspcv 3580 |
. . . . . . . . . . . . . . . . . 18
β’ ((πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β (Filβπ) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (πΉ β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))))) |
122 | 116, 121 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (πΉ β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))) β π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))))) |
123 | 114, 122 | mpid 44 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))))) |
124 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) β π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) |
125 | | simplrl 776 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) β π β π½) |
126 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β π΄ β π) |
127 | 126 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) β π΄ β π) |
128 | 113, 55 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π β π) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) β (π β π) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) |
130 | | fclsopni 23382 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) β§ (π β π½ β§ π΄ β π β§ (π β π) β (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) β (π β© (π β π)) β β
) |
131 | 124, 125,
127, 129, 130 | syl13anc 1373 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β§ π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯}))))) β (π β© (π β π)) β β
) |
132 | 131 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (π΄ β (π½ fClus (πfilGen(fiβ(πΉ βͺ {π₯ β π« π β£ (π β π) β π₯})))) β (π β© (π β π)) β β
)) |
133 | 123, 132 | syld 47 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (π β© (π β π)) β β
)) |
134 | 133 | necon2bd 2960 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β ((π β© (π β π)) = β
β Β¬ βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)))) |
135 | 29, 134 | mpi 20 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ (π β π½ β§ (π΄ β π β§ Β¬ π β πΉ))) β Β¬ βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π))) |
136 | 135 | anassrs 469 |
. . . . . . . . . . . 12
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ π β π½) β§ (π΄ β π β§ Β¬ π β πΉ)) β Β¬ βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π))) |
137 | 136 | expr 458 |
. . . . . . . . . . 11
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ π β π½) β§ π΄ β π) β (Β¬ π β πΉ β Β¬ βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)))) |
138 | 137 | con4d 115 |
. . . . . . . . . 10
β’ ((((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ π β π½) β§ π΄ β π) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β π β πΉ)) |
139 | 138 | ex 414 |
. . . . . . . . 9
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ π β π½) β (π΄ β π β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β π β πΉ))) |
140 | 139 | com23 86 |
. . . . . . . 8
β’ (((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β§ π β π½) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (π΄ β π β π β πΉ))) |
141 | 140 | ralrimdva 3152 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β βπ β π½ (π΄ β π β π β πΉ))) |
142 | | simprr 772 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β π΄ β π) |
143 | 141, 142 | jctild 527 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β (π΄ β π β§ βπ β π½ (π΄ β π β π β πΉ)))) |
144 | | simprl 770 |
. . . . . . . 8
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β π½ β Top) |
145 | 144, 4 | sylib 217 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β π½ β (TopOnβπ)) |
146 | | simpl 484 |
. . . . . . 7
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β πΉ β (Filβπ)) |
147 | | flimopn 23342 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β π β πΉ)))) |
148 | 145, 146,
147 | syl2anc 585 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β π β πΉ)))) |
149 | 143, 148 | sylibrd 259 |
. . . . 5
β’ ((πΉ β (Filβπ) β§ (π½ β Top β§ π΄ β π)) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β π΄ β (π½ fLim πΉ))) |
150 | 149 | ex 414 |
. . . 4
β’ (πΉ β (Filβπ) β ((π½ β Top β§ π΄ β π) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β π΄ β (π½ fLim πΉ)))) |
151 | 150 | com23 86 |
. . 3
β’ (πΉ β (Filβπ) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β ((π½ β Top β§ π΄ β π) β π΄ β (π½ fLim πΉ)))) |
152 | 28, 151 | mpdd 43 |
. 2
β’ (πΉ β (Filβπ) β (βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)) β π΄ β (π½ fLim πΉ))) |
153 | 15, 152 | impbid2 225 |
1
β’ (πΉ β (Filβπ) β (π΄ β (π½ fLim πΉ) β βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)))) |