| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2731 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
| 2 | 1 | flimelbas 23693 |
. . . . . 6
β’ (π₯ β (π½ fLim πΊ) β π₯ β βͺ π½) |
| 3 | 2 | adantl 481 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β π₯ β βͺ π½) |
| 4 | | simpl1 1190 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β π½ β (TopOnβπ)) |
| 5 | | toponuni 22637 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
| 6 | 4, 5 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β π = βͺ π½) |
| 7 | 3, 6 | eleqtrrd 2835 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β π₯ β π) |
| 8 | | flimneiss 23691 |
. . . . . 6
β’ (π₯ β (π½ fLim πΊ) β ((neiβπ½)β{π₯}) β πΊ) |
| 9 | 8 | adantl 481 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β ((neiβπ½)β{π₯}) β πΊ) |
| 10 | | simpl3 1192 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β πΊ β πΉ) |
| 11 | 9, 10 | sstrd 3992 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β ((neiβπ½)β{π₯}) β πΉ) |
| 12 | | simpl2 1191 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β πΉ β (Filβπ)) |
| 13 | | elflim 23696 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π₯ β (π½ fLim πΉ) β (π₯ β π β§ ((neiβπ½)β{π₯}) β πΉ))) |
| 14 | 4, 12, 13 | syl2anc 583 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β (π₯ β (π½ fLim πΉ) β (π₯ β π β§ ((neiβπ½)β{π₯}) β πΉ))) |
| 15 | 7, 11, 14 | mpbir2and 710 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β§ π₯ β (π½ fLim πΊ)) β π₯ β (π½ fLim πΉ)) |
| 16 | 15 | ex 412 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β (π₯ β (π½ fLim πΊ) β π₯ β (π½ fLim πΉ))) |
| 17 | 16 | ssrdv 3988 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β (π½ fLim πΊ) β (π½ fLim πΉ)) |
