Step | Hyp | Ref
| Expression |
1 | | flimtop 23476 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β π½ β Top) |
2 | | eqid 2732 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
3 | 2 | flimelbas 23479 |
. . . . . . 7
β’ (π΄ β (π½ fLim πΉ) β π΄ β βͺ π½) |
4 | 3 | snssd 4812 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β {π΄} β βͺ π½) |
5 | 2 | clsss3 22570 |
. . . . . 6
β’ ((π½ β Top β§ {π΄} β βͺ π½)
β ((clsβπ½)β{π΄}) β βͺ
π½) |
6 | 1, 4, 5 | syl2anc 584 |
. . . . 5
β’ (π΄ β (π½ fLim πΉ) β ((clsβπ½)β{π΄}) β βͺ
π½) |
7 | 6 | sselda 3982 |
. . . 4
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π₯ β βͺ π½) |
8 | | simpll 765 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π΄ β (π½ fLim πΉ)) |
9 | 8, 1 | syl 17 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π½ β Top) |
10 | | simprl 769 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β π½) |
11 | 1 | adantr 481 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π½ β Top) |
12 | 4 | adantr 481 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β {π΄} β βͺ π½) |
13 | | simpr 485 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π₯ β ((clsβπ½)β{π΄})) |
14 | 11, 12, 13 | 3jca 1128 |
. . . . . . . . 9
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β (π½ β Top β§ {π΄} β βͺ π½ β§ π₯ β ((clsβπ½)β{π΄}))) |
15 | 2 | clsndisj 22586 |
. . . . . . . . . 10
β’ (((π½ β Top β§ {π΄} β βͺ π½
β§ π₯ β
((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β (π¦ β© {π΄}) β β
) |
16 | | disjsn 4715 |
. . . . . . . . . . 11
β’ ((π¦ β© {π΄}) = β
β Β¬ π΄ β π¦) |
17 | 16 | necon2abii 2991 |
. . . . . . . . . 10
β’ (π΄ β π¦ β (π¦ β© {π΄}) β β
) |
18 | 15, 17 | sylibr 233 |
. . . . . . . . 9
β’ (((π½ β Top β§ {π΄} β βͺ π½
β§ π₯ β
((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π΄ β π¦) |
19 | 14, 18 | sylan 580 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π΄ β π¦) |
20 | | opnneip 22630 |
. . . . . . . 8
β’ ((π½ β Top β§ π¦ β π½ β§ π΄ β π¦) β π¦ β ((neiβπ½)β{π΄})) |
21 | 9, 10, 19, 20 | syl3anc 1371 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β ((neiβπ½)β{π΄})) |
22 | | flimnei 23478 |
. . . . . . 7
β’ ((π΄ β (π½ fLim πΉ) β§ π¦ β ((neiβπ½)β{π΄})) β π¦ β πΉ) |
23 | 8, 21, 22 | syl2anc 584 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β πΉ) |
24 | 23 | expr 457 |
. . . . 5
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ π¦ β π½) β (π₯ β π¦ β π¦ β πΉ)) |
25 | 24 | ralrimiva 3146 |
. . . 4
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)) |
26 | | toptopon2 22427 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
27 | 11, 26 | sylib 217 |
. . . . 5
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π½ β (TopOnββͺ π½)) |
28 | 2 | flimfil 23480 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β πΉ β (Filββͺ π½)) |
29 | 28 | adantr 481 |
. . . . 5
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β πΉ β (Filββͺ π½)) |
30 | | flimopn 23486 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ β
(Filββͺ π½)) β (π₯ β (π½ fLim πΉ) β (π₯ β βͺ π½ β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
31 | 27, 29, 30 | syl2anc 584 |
. . . 4
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β (π₯ β (π½ fLim πΉ) β (π₯ β βͺ π½ β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
32 | 7, 25, 31 | mpbir2and 711 |
. . 3
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π₯ β (π½ fLim πΉ)) |
33 | 32 | ex 413 |
. 2
β’ (π΄ β (π½ fLim πΉ) β (π₯ β ((clsβπ½)β{π΄}) β π₯ β (π½ fLim πΉ))) |
34 | 33 | ssrdv 3988 |
1
β’ (π΄ β (π½ fLim πΉ) β ((clsβπ½)β{π΄}) β (π½ fLim πΉ)) |