Step | Hyp | Ref
| Expression |
1 | | fbflim.3 |
. . 3
β’ πΉ = (πfilGenπ΅) |
2 | 1 | fbflim 23700 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ¦ β π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦)))) |
3 | | topontop 22635 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π½ β Top) |
4 | 3 | ad2antrr 724 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β π½ β Top) |
5 | | simpr 485 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β π΄ β π) |
6 | | toponuni 22636 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
7 | 6 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β π = βͺ π½) |
8 | 5, 7 | eleqtrd 2835 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β π΄ β βͺ π½) |
9 | | eqid 2732 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
10 | 9 | isneip 22829 |
. . . . . . . 8
β’ ((π½ β Top β§ π΄ β βͺ π½)
β (π β
((neiβπ½)β{π΄}) β (π β βͺ π½ β§ βπ¦ β π½ (π΄ β π¦ β§ π¦ β π)))) |
11 | 4, 8, 10 | syl2anc 584 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (π β ((neiβπ½)β{π΄}) β (π β βͺ π½ β§ βπ¦ β π½ (π΄ β π¦ β§ π¦ β π)))) |
12 | | simpr 485 |
. . . . . . 7
β’ ((π β βͺ π½
β§ βπ¦ β π½ (π΄ β π¦ β§ π¦ β π)) β βπ¦ β π½ (π΄ β π¦ β§ π¦ β π)) |
13 | 11, 12 | syl6bi 252 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (π β ((neiβπ½)β{π΄}) β βπ¦ β π½ (π΄ β π¦ β§ π¦ β π))) |
14 | | r19.29 3114 |
. . . . . . . 8
β’
((βπ¦ β
π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β§ βπ¦ β π½ (π΄ β π¦ β§ π¦ β π)) β βπ¦ β π½ ((π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β§ (π΄ β π¦ β§ π¦ β π))) |
15 | | pm3.45 622 |
. . . . . . . . . . 11
β’ ((π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β ((π΄ β π¦ β§ π¦ β π) β (βπ₯ β π΅ π₯ β π¦ β§ π¦ β π))) |
16 | 15 | imp 407 |
. . . . . . . . . 10
β’ (((π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β§ (π΄ β π¦ β§ π¦ β π)) β (βπ₯ β π΅ π₯ β π¦ β§ π¦ β π)) |
17 | | sstr2 3989 |
. . . . . . . . . . . . 13
β’ (π₯ β π¦ β (π¦ β π β π₯ β π)) |
18 | 17 | com12 32 |
. . . . . . . . . . . 12
β’ (π¦ β π β (π₯ β π¦ β π₯ β π)) |
19 | 18 | reximdv 3170 |
. . . . . . . . . . 11
β’ (π¦ β π β (βπ₯ β π΅ π₯ β π¦ β βπ₯ β π΅ π₯ β π)) |
20 | 19 | impcom 408 |
. . . . . . . . . 10
β’
((βπ₯ β
π΅ π₯ β π¦ β§ π¦ β π) β βπ₯ β π΅ π₯ β π) |
21 | 16, 20 | syl 17 |
. . . . . . . . 9
β’ (((π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β§ (π΄ β π¦ β§ π¦ β π)) β βπ₯ β π΅ π₯ β π) |
22 | 21 | rexlimivw 3151 |
. . . . . . . 8
β’
(βπ¦ β
π½ ((π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β§ (π΄ β π¦ β§ π¦ β π)) β βπ₯ β π΅ π₯ β π) |
23 | 14, 22 | syl 17 |
. . . . . . 7
β’
((βπ¦ β
π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β§ βπ¦ β π½ (π΄ β π¦ β§ π¦ β π)) β βπ₯ β π΅ π₯ β π) |
24 | 23 | ex 413 |
. . . . . 6
β’
(βπ¦ β
π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β (βπ¦ β π½ (π΄ β π¦ β§ π¦ β π) β βπ₯ β π΅ π₯ β π)) |
25 | 13, 24 | syl9 77 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (βπ¦ β π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β (π β ((neiβπ½)β{π΄}) β βπ₯ β π΅ π₯ β π))) |
26 | 25 | ralrimdv 3152 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (βπ¦ β π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π)) |
27 | 4 | adantr 481 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π¦ β π½ β§ π΄ β π¦)) β π½ β Top) |
28 | | simprl 769 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π¦ β π½ β§ π΄ β π¦)) β π¦ β π½) |
29 | | simprr 771 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π¦ β π½ β§ π΄ β π¦)) β π΄ β π¦) |
30 | | opnneip 22843 |
. . . . . . . . 9
β’ ((π½ β Top β§ π¦ β π½ β§ π΄ β π¦) β π¦ β ((neiβπ½)β{π΄})) |
31 | 27, 28, 29, 30 | syl3anc 1371 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π¦ β π½ β§ π΄ β π¦)) β π¦ β ((neiβπ½)β{π΄})) |
32 | | sseq2 4008 |
. . . . . . . . . 10
β’ (π = π¦ β (π₯ β π β π₯ β π¦)) |
33 | 32 | rexbidv 3178 |
. . . . . . . . 9
β’ (π = π¦ β (βπ₯ β π΅ π₯ β π β βπ₯ β π΅ π₯ β π¦)) |
34 | 33 | rspcv 3608 |
. . . . . . . 8
β’ (π¦ β ((neiβπ½)β{π΄}) β (βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π β βπ₯ β π΅ π₯ β π¦)) |
35 | 31, 34 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ (π¦ β π½ β§ π΄ β π¦)) β (βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π β βπ₯ β π΅ π₯ β π¦)) |
36 | 35 | expr 457 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ π¦ β π½) β (π΄ β π¦ β (βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π β βπ₯ β π΅ π₯ β π¦))) |
37 | 36 | com23 86 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β§ π¦ β π½) β (βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π β (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦))) |
38 | 37 | ralrimdva 3154 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π β βπ¦ β π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦))) |
39 | 26, 38 | impbid 211 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β§ π΄ β π) β (βπ¦ β π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦) β βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π)) |
40 | 39 | pm5.32da 579 |
. 2
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β ((π΄ β π β§ βπ¦ β π½ (π΄ β π¦ β βπ₯ β π΅ π₯ β π¦)) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π))) |
41 | 2, 40 | bitrd 278 |
1
β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π))) |