Step | Hyp | Ref
| Expression |
1 | | cnpf2 22754 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
2 | 1 | 3expa 1119 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
3 | 2 | 3adantl3 1169 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:πβΆπ) |
4 | | cnpflfi 23503 |
. . . . . . 7
β’ ((π΄ β (π½ fLim π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)) |
5 | 4 | expcom 415 |
. . . . . 6
β’ (πΉ β ((π½ CnP πΎ)βπ΄) β (π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))) |
6 | 5 | ralrimivw 3151 |
. . . . 5
β’ (πΉ β ((π½ CnP πΎ)βπ΄) β βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))) |
7 | 6 | adantl 483 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))) |
8 | 3, 7 | jca 513 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)))) |
9 | 8 | ex 414 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))))) |
10 | | simpl1 1192 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π½ β (TopOnβπ)) |
11 | | simpl3 1194 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π΄ β π) |
12 | | neiflim 23478 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β (π½ fLim ((neiβπ½)β{π΄}))) |
13 | 10, 11, 12 | syl2anc 585 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β π΄ β (π½ fLim ((neiβπ½)β{π΄}))) |
14 | 11 | snssd 4813 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β {π΄} β π) |
15 | 11 | snn0d 4780 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β {π΄} β β
) |
16 | | neifil 23384 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ {π΄} β π β§ {π΄} β β
) β ((neiβπ½)β{π΄}) β (Filβπ)) |
17 | 10, 14, 15, 16 | syl3anc 1372 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β ((neiβπ½)β{π΄}) β (Filβπ)) |
18 | | oveq2 7417 |
. . . . . . . . 9
β’ (π = ((neiβπ½)β{π΄}) β (π½ fLim π) = (π½ fLim ((neiβπ½)β{π΄}))) |
19 | 18 | eleq2d 2820 |
. . . . . . . 8
β’ (π = ((neiβπ½)β{π΄}) β (π΄ β (π½ fLim π) β π΄ β (π½ fLim ((neiβπ½)β{π΄})))) |
20 | | oveq2 7417 |
. . . . . . . . . 10
β’ (π = ((neiβπ½)β{π΄}) β (πΎ fLimf π) = (πΎ fLimf ((neiβπ½)β{π΄}))) |
21 | 20 | fveq1d 6894 |
. . . . . . . . 9
β’ (π = ((neiβπ½)β{π΄}) β ((πΎ fLimf π)βπΉ) = ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ)) |
22 | 21 | eleq2d 2820 |
. . . . . . . 8
β’ (π = ((neiβπ½)β{π΄}) β ((πΉβπ΄) β ((πΎ fLimf π)βπΉ) β (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ))) |
23 | 19, 22 | imbi12d 345 |
. . . . . . 7
β’ (π = ((neiβπ½)β{π΄}) β ((π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)) β (π΄ β (π½ fLim ((neiβπ½)β{π΄})) β (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ)))) |
24 | 23 | rspcv 3609 |
. . . . . 6
β’
(((neiβπ½)β{π΄}) β (Filβπ) β (βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)) β (π΄ β (π½ fLim ((neiβπ½)β{π΄})) β (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ)))) |
25 | 17, 24 | syl 17 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)) β (π΄ β (π½ fLim ((neiβπ½)β{π΄})) β (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ)))) |
26 | 13, 25 | mpid 44 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ πΉ:πβΆπ) β (βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ)) β (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ))) |
27 | 26 | imdistanda 573 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β ((πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))) β (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ)))) |
28 | | eqid 2733 |
. . . 4
β’
((neiβπ½)β{π΄}) = ((neiβπ½)β{π΄}) |
29 | 28 | cnpflf2 23504 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf ((neiβπ½)β{π΄}))βπΉ)))) |
30 | 27, 29 | sylibrd 259 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β ((πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))) β πΉ β ((π½ CnP πΎ)βπ΄))) |
31 | 9, 30 | impbid 211 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))))) |