Step | Hyp | Ref
| Expression |
1 | | flimtop 23469 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β π½ β Top) |
2 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
3 | 2 | flimelbas 23472 |
. . . . . . 7
β’ (π΄ β (π½ fLim πΉ) β π΄ β βͺ π½) |
4 | 3 | snssd 4813 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β {π΄} β βͺ π½) |
5 | 2 | clsss3 22563 |
. . . . . 6
β’ ((π½ β Top β§ {π΄} β βͺ π½)
β ((clsβπ½)β{π΄}) β βͺ
π½) |
6 | 1, 4, 5 | syl2anc 585 |
. . . . 5
β’ (π΄ β (π½ fLim πΉ) β ((clsβπ½)β{π΄}) β βͺ
π½) |
7 | 6 | sselda 3983 |
. . . 4
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π₯ β βͺ π½) |
8 | | simpll 766 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π΄ β (π½ fLim πΉ)) |
9 | 8, 1 | syl 17 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π½ β Top) |
10 | | simprl 770 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β π½) |
11 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π½ β Top) |
12 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β {π΄} β βͺ π½) |
13 | | simpr 486 |
. . . . . . . . . 10
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π₯ β ((clsβπ½)β{π΄})) |
14 | 11, 12, 13 | 3jca 1129 |
. . . . . . . . 9
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β (π½ β Top β§ {π΄} β βͺ π½ β§ π₯ β ((clsβπ½)β{π΄}))) |
15 | 2 | clsndisj 22579 |
. . . . . . . . . 10
β’ (((π½ β Top β§ {π΄} β βͺ π½
β§ π₯ β
((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β (π¦ β© {π΄}) β β
) |
16 | | disjsn 4716 |
. . . . . . . . . . 11
β’ ((π¦ β© {π΄}) = β
β Β¬ π΄ β π¦) |
17 | 16 | necon2abii 2992 |
. . . . . . . . . 10
β’ (π΄ β π¦ β (π¦ β© {π΄}) β β
) |
18 | 15, 17 | sylibr 233 |
. . . . . . . . 9
β’ (((π½ β Top β§ {π΄} β βͺ π½
β§ π₯ β
((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π΄ β π¦) |
19 | 14, 18 | sylan 581 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π΄ β π¦) |
20 | | opnneip 22623 |
. . . . . . . 8
β’ ((π½ β Top β§ π¦ β π½ β§ π΄ β π¦) β π¦ β ((neiβπ½)β{π΄})) |
21 | 9, 10, 19, 20 | syl3anc 1372 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β ((neiβπ½)β{π΄})) |
22 | | flimnei 23471 |
. . . . . . 7
β’ ((π΄ β (π½ fLim πΉ) β§ π¦ β ((neiβπ½)β{π΄})) β π¦ β πΉ) |
23 | 8, 21, 22 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β πΉ) |
24 | 23 | expr 458 |
. . . . 5
β’ (((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β§ π¦ β π½) β (π₯ β π¦ β π¦ β πΉ)) |
25 | 24 | ralrimiva 3147 |
. . . 4
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)) |
26 | | toptopon2 22420 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
27 | 11, 26 | sylib 217 |
. . . . 5
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π½ β (TopOnββͺ π½)) |
28 | 2 | flimfil 23473 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β πΉ β (Filββͺ π½)) |
29 | 28 | adantr 482 |
. . . . 5
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β πΉ β (Filββͺ π½)) |
30 | | flimopn 23479 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ β
(Filββͺ π½)) β (π₯ β (π½ fLim πΉ) β (π₯ β βͺ π½ β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
31 | 27, 29, 30 | syl2anc 585 |
. . . 4
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β (π₯ β (π½ fLim πΉ) β (π₯ β βͺ π½ β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
32 | 7, 25, 31 | mpbir2and 712 |
. . 3
β’ ((π΄ β (π½ fLim πΉ) β§ π₯ β ((clsβπ½)β{π΄})) β π₯ β (π½ fLim πΉ)) |
33 | 32 | ex 414 |
. 2
β’ (π΄ β (π½ fLim πΉ) β (π₯ β ((clsβπ½)β{π΄}) β π₯ β (π½ fLim πΉ))) |
34 | 33 | ssrdv 3989 |
1
β’ (π΄ β (π½ fLim πΉ) β ((clsβπ½)β{π΄}) β (π½ fLim πΉ)) |