Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
2 | | eqid 2733 |
. . . . 5
β’ βͺ πΎ =
βͺ πΎ |
3 | 1, 2 | cnpf 22621 |
. . . 4
β’ (πΉ β ((π½ CnP πΎ)βπ΄) β πΉ:βͺ π½βΆβͺ πΎ) |
4 | 3 | adantl 483 |
. . 3
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΉ:βͺ π½βΆβͺ πΎ) |
5 | 1 | flimelbas 23342 |
. . . 4
β’ (π΄ β (π½ fLim πΏ) β π΄ β βͺ π½) |
6 | 5 | adantr 482 |
. . 3
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π΄ β βͺ π½) |
7 | 4, 6 | ffvelcdmd 7040 |
. 2
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β βͺ πΎ) |
8 | | simplr 768 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β πΉ β ((π½ CnP πΎ)βπ΄)) |
9 | | simprl 770 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β π₯ β πΎ) |
10 | | simprr 772 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β (πΉβπ΄) β π₯) |
11 | | cnpimaex 22630 |
. . . . . 6
β’ ((πΉ β ((π½ CnP πΎ)βπ΄) β§ π₯ β πΎ β§ (πΉβπ΄) β π₯) β βπ¦ β π½ (π΄ β π¦ β§ (πΉ β π¦) β π₯)) |
12 | 8, 9, 10, 11 | syl3anc 1372 |
. . . . 5
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β βπ¦ β π½ (π΄ β π¦ β§ (πΉ β π¦) β π₯)) |
13 | | anass 470 |
. . . . . . 7
β’ (((π¦ β π½ β§ π΄ β π¦) β§ (πΉ β π¦) β π₯) β (π¦ β π½ β§ (π΄ β π¦ β§ (πΉ β π¦) β π₯))) |
14 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π΄ β (π½ fLim πΏ)) |
15 | | flimtop 23339 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β (π½ fLim πΏ) β π½ β Top) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π½ β Top) |
17 | | toptopon2 22290 |
. . . . . . . . . . . . . . 15
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
18 | 16, 17 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β π½ β (TopOnββͺ π½)) |
19 | 1 | flimfil 23343 |
. . . . . . . . . . . . . . 15
β’ (π΄ β (π½ fLim πΏ) β πΏ β (Filββͺ π½)) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΏ β (Filββͺ π½)) |
21 | | flimopn 23349 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnββͺ π½)
β§ πΏ β
(Filββͺ π½)) β (π΄ β (π½ fLim πΏ) β (π΄ β βͺ π½ β§ βπ¦ β π½ (π΄ β π¦ β π¦ β πΏ)))) |
22 | 18, 20, 21 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (π΄ β (π½ fLim πΏ) β (π΄ β βͺ π½ β§ βπ¦ β π½ (π΄ β π¦ β π¦ β πΏ)))) |
23 | 14, 22 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (π΄ β βͺ π½ β§ βπ¦ β π½ (π΄ β π¦ β π¦ β πΏ))) |
24 | 23 | simprd 497 |
. . . . . . . . . . 11
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β βπ¦ β π½ (π΄ β π¦ β π¦ β πΏ)) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β βπ¦ β π½ (π΄ β π¦ β π¦ β πΏ)) |
26 | 25 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β§ π¦ β π½) β (π΄ β π¦ β π¦ β πΏ)) |
27 | 26 | expimpd 455 |
. . . . . . . 8
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β ((π¦ β π½ β§ π΄ β π¦) β π¦ β πΏ)) |
28 | 27 | anim1d 612 |
. . . . . . 7
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β (((π¦ β π½ β§ π΄ β π¦) β§ (πΉ β π¦) β π₯) β (π¦ β πΏ β§ (πΉ β π¦) β π₯))) |
29 | 13, 28 | biimtrrid 242 |
. . . . . 6
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β ((π¦ β π½ β§ (π΄ β π¦ β§ (πΉ β π¦) β π₯)) β (π¦ β πΏ β§ (πΉ β π¦) β π₯))) |
30 | 29 | reximdv2 3158 |
. . . . 5
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β (βπ¦ β π½ (π΄ β π¦ β§ (πΉ β π¦) β π₯) β βπ¦ β πΏ (πΉ β π¦) β π₯)) |
31 | 12, 30 | mpd 15 |
. . . 4
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ (π₯ β πΎ β§ (πΉβπ΄) β π₯)) β βπ¦ β πΏ (πΉ β π¦) β π₯) |
32 | 31 | expr 458 |
. . 3
β’ (((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β§ π₯ β πΎ) β ((πΉβπ΄) β π₯ β βπ¦ β πΏ (πΉ β π¦) β π₯)) |
33 | 32 | ralrimiva 3140 |
. 2
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β βπ₯ β πΎ ((πΉβπ΄) β π₯ β βπ¦ β πΏ (πΉ β π¦) β π₯)) |
34 | | cnptop2 22617 |
. . . . 5
β’ (πΉ β ((π½ CnP πΎ)βπ΄) β πΎ β Top) |
35 | 34 | adantl 483 |
. . . 4
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΎ β Top) |
36 | | toptopon2 22290 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
37 | 35, 36 | sylib 217 |
. . 3
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β πΎ β (TopOnββͺ πΎ)) |
38 | | isflf 23367 |
. . 3
β’ ((πΎ β (TopOnββͺ πΎ)
β§ πΏ β
(Filββͺ π½) β§ πΉ:βͺ π½βΆβͺ πΎ)
β ((πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ) β ((πΉβπ΄) β βͺ πΎ β§ βπ₯ β πΎ ((πΉβπ΄) β π₯ β βπ¦ β πΏ (πΉ β π¦) β π₯)))) |
39 | 37, 20, 4, 38 | syl3anc 1372 |
. 2
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β ((πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ) β ((πΉβπ΄) β βͺ πΎ β§ βπ₯ β πΎ ((πΉβπ΄) β π₯ β βπ¦ β πΏ (πΉ β π¦) β π₯)))) |
40 | 7, 33, 39 | mpbir2and 712 |
1
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)) |