Step | Hyp | Ref
| Expression |
1 | | elflim 23475 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) |
2 | | dfss3 3971 |
. . . 4
β’
(((neiβπ½)β{π΄}) β πΉ β βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ) |
3 | | topontop 22415 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π½ β Top) |
4 | 3 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β π½ β Top) |
5 | | opnneip 22623 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π₯ β π½ β§ π΄ β π₯) β π₯ β ((neiβπ½)β{π΄})) |
6 | 5 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π½ β Top β§ (π₯ β π½ β§ π΄ β π₯)) β π₯ β ((neiβπ½)β{π΄})) |
7 | 4, 6 | sylan 581 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ (π₯ β π½ β§ π΄ β π₯)) β π₯ β ((neiβπ½)β{π΄})) |
8 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (π¦ β πΉ β π₯ β πΉ)) |
9 | 8 | rspcv 3609 |
. . . . . . . . 9
β’ (π₯ β ((neiβπ½)β{π΄}) β (βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ β π₯ β πΉ)) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ (π₯ β π½ β§ π΄ β π₯)) β (βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ β π₯ β πΉ)) |
11 | 10 | expr 458 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π₯ β π½) β (π΄ β π₯ β (βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ β π₯ β πΉ))) |
12 | 11 | com23 86 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π₯ β π½) β (βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ β (π΄ β π₯ β π₯ β πΉ))) |
13 | 12 | ralrimdva 3155 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β (βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ β βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ))) |
14 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π¦ β ((neiβπ½)β{π΄})) |
15 | 3 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π½ β Top) |
16 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π΄ β π) |
17 | | toponuni 22416 |
. . . . . . . . . . . . . 14
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
18 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π = βͺ π½) |
19 | 16, 18 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π΄ β βͺ π½) |
20 | 19 | snssd 4813 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β {π΄} β βͺ π½) |
21 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
22 | 21 | neii1 22610 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π¦ β ((neiβπ½)β{π΄})) β π¦ β βͺ π½) |
23 | 4, 22 | sylan 581 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π¦ β βͺ π½) |
24 | 21 | neiint 22608 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ {π΄} β βͺ π½
β§ π¦ β βͺ π½)
β (π¦ β
((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ¦))) |
25 | 15, 20, 23, 24 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β (π¦ β ((neiβπ½)β{π΄}) β {π΄} β ((intβπ½)βπ¦))) |
26 | 14, 25 | mpbid 231 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β {π΄} β ((intβπ½)βπ¦)) |
27 | | snssg 4788 |
. . . . . . . . . 10
β’ (π΄ β π β (π΄ β ((intβπ½)βπ¦) β {π΄} β ((intβπ½)βπ¦))) |
28 | 27 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β (π΄ β ((intβπ½)βπ¦) β {π΄} β ((intβπ½)βπ¦))) |
29 | 26, 28 | mpbird 257 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π΄ β ((intβπ½)βπ¦)) |
30 | 21 | ntropn 22553 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π¦ β βͺ π½)
β ((intβπ½)βπ¦) β π½) |
31 | 15, 23, 30 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β ((intβπ½)βπ¦) β π½) |
32 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π₯ = ((intβπ½)βπ¦) β (π΄ β π₯ β π΄ β ((intβπ½)βπ¦))) |
33 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π₯ = ((intβπ½)βπ¦) β (π₯ β πΉ β ((intβπ½)βπ¦) β πΉ)) |
34 | 32, 33 | imbi12d 345 |
. . . . . . . . . 10
β’ (π₯ = ((intβπ½)βπ¦) β ((π΄ β π₯ β π₯ β πΉ) β (π΄ β ((intβπ½)βπ¦) β ((intβπ½)βπ¦) β πΉ))) |
35 | 34 | rspcv 3609 |
. . . . . . . . 9
β’
(((intβπ½)βπ¦) β π½ β (βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ) β (π΄ β ((intβπ½)βπ¦) β ((intβπ½)βπ¦) β πΉ))) |
36 | 31, 35 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β (βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ) β (π΄ β ((intβπ½)βπ¦) β ((intβπ½)βπ¦) β πΉ))) |
37 | 29, 36 | mpid 44 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β (βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ) β ((intβπ½)βπ¦) β πΉ)) |
38 | | simpllr 775 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β πΉ β (Filβπ)) |
39 | 21 | ntrss2 22561 |
. . . . . . . . 9
β’ ((π½ β Top β§ π¦ β βͺ π½)
β ((intβπ½)βπ¦) β π¦) |
40 | 15, 23, 39 | syl2anc 585 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β ((intβπ½)βπ¦) β π¦) |
41 | 23, 18 | sseqtrrd 4024 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β π¦ β π) |
42 | | filss 23357 |
. . . . . . . . . 10
β’ ((πΉ β (Filβπ) β§ (((intβπ½)βπ¦) β πΉ β§ π¦ β π β§ ((intβπ½)βπ¦) β π¦)) β π¦ β πΉ) |
43 | 42 | 3exp2 1355 |
. . . . . . . . 9
β’ (πΉ β (Filβπ) β (((intβπ½)βπ¦) β πΉ β (π¦ β π β (((intβπ½)βπ¦) β π¦ β π¦ β πΉ)))) |
44 | 43 | com24 95 |
. . . . . . . 8
β’ (πΉ β (Filβπ) β (((intβπ½)βπ¦) β π¦ β (π¦ β π β (((intβπ½)βπ¦) β πΉ β π¦ β πΉ)))) |
45 | 38, 40, 41, 44 | syl3c 66 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β (((intβπ½)βπ¦) β πΉ β π¦ β πΉ)) |
46 | 37, 45 | syld 47 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β§ π¦ β ((neiβπ½)β{π΄})) β (βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ) β π¦ β πΉ)) |
47 | 46 | ralrimdva 3155 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β (βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ) β βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ)) |
48 | 13, 47 | impbid 211 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β (βπ¦ β ((neiβπ½)β{π΄})π¦ β πΉ β βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ))) |
49 | 2, 48 | bitrid 283 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β§ π΄ β π) β (((neiβπ½)β{π΄}) β πΉ β βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ))) |
50 | 49 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β ((π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ) β (π΄ β π β§ βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ)))) |
51 | 1, 50 | bitrd 279 |
1
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ)))) |