Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
2 | 1 | flimelbas 23472 |
. . . . . 6
β’ (π₯ β (πΎ fLim πΉ) β π₯ β βͺ πΎ) |
3 | 2 | adantl 483 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π₯ β βͺ πΎ) |
4 | | simpl2 1193 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β πΉ β (Filβπ)) |
5 | | filunibas 23385 |
. . . . . . 7
β’ (πΉ β (Filβπ) β βͺ πΉ =
π) |
6 | 4, 5 | syl 17 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β βͺ πΉ = π) |
7 | 1 | flimfil 23473 |
. . . . . . . 8
β’ (π₯ β (πΎ fLim πΉ) β πΉ β (Filββͺ πΎ)) |
8 | 7 | adantl 483 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β πΉ β (Filββͺ πΎ)) |
9 | | filunibas 23385 |
. . . . . . 7
β’ (πΉ β (Filββͺ πΎ)
β βͺ πΉ = βͺ πΎ) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β βͺ πΉ = βͺ
πΎ) |
11 | 6, 10 | eqtr3d 2775 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π = βͺ πΎ) |
12 | 3, 11 | eleqtrrd 2837 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π₯ β π) |
13 | | simpl1 1192 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π½ β (TopOnβπ)) |
14 | | topontop 22415 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
15 | 13, 14 | syl 17 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π½ β Top) |
16 | | flimtop 23469 |
. . . . . . 7
β’ (π₯ β (πΎ fLim πΉ) β πΎ β Top) |
17 | 16 | adantl 483 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β πΎ β Top) |
18 | | toponuni 22416 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
19 | 13, 18 | syl 17 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π = βͺ π½) |
20 | 19, 11 | eqtr3d 2775 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β βͺ π½ = βͺ
πΎ) |
21 | | simpl3 1194 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π½ β πΎ) |
22 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
23 | 22, 1 | topssnei 22628 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ βͺ π½ =
βͺ πΎ) β§ π½ β πΎ) β ((neiβπ½)β{π₯}) β ((neiβπΎ)β{π₯})) |
24 | 15, 17, 20, 21, 23 | syl31anc 1374 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β ((neiβπ½)β{π₯}) β ((neiβπΎ)β{π₯})) |
25 | | flimneiss 23470 |
. . . . . 6
β’ (π₯ β (πΎ fLim πΉ) β ((neiβπΎ)β{π₯}) β πΉ) |
26 | 25 | adantl 483 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β ((neiβπΎ)β{π₯}) β πΉ) |
27 | 24, 26 | sstrd 3993 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β ((neiβπ½)β{π₯}) β πΉ) |
28 | | elflim 23475 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π₯ β (π½ fLim πΉ) β (π₯ β π β§ ((neiβπ½)β{π₯}) β πΉ))) |
29 | 13, 4, 28 | syl2anc 585 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β (π₯ β (π½ fLim πΉ) β (π₯ β π β§ ((neiβπ½)β{π₯}) β πΉ))) |
30 | 12, 27, 29 | mpbir2and 712 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β§ π₯ β (πΎ fLim πΉ)) β π₯ β (π½ fLim πΉ)) |
31 | 30 | ex 414 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β (π₯ β (πΎ fLim πΉ) β π₯ β (π½ fLim πΉ))) |
32 | 31 | ssrdv 3989 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β (πΎ fLim πΉ) β (π½ fLim πΉ)) |