Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. 2
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β πΈ β (βMetβπ)) |
2 | | simpl1 1192 |
. . . . 5
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β π· β (CMetβπ)) |
3 | | fmcncfil.1 |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
4 | 3 | cmetcvg 24665 |
. . . . . 6
β’ ((π· β (CMetβπ) β§ π΅ β (CauFilβπ·)) β (π½ fLim π΅) β β
) |
5 | | n0 4311 |
. . . . . 6
β’ ((π½ fLim π΅) β β
β βπ₯ π₯ β (π½ fLim π΅)) |
6 | 4, 5 | sylib 217 |
. . . . 5
β’ ((π· β (CMetβπ) β§ π΅ β (CauFilβπ·)) β βπ₯ π₯ β (π½ fLim π΅)) |
7 | 2, 6 | sylancom 589 |
. . . 4
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β βπ₯ π₯ β (π½ fLim π΅)) |
8 | | cmetmet 24666 |
. . . . . . . 8
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
9 | | metxmet 23703 |
. . . . . . . 8
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
10 | 2, 8, 9 | 3syl 18 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β π· β (βMetβπ)) |
11 | | cfilfil 24647 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π΅ β (CauFilβπ·)) β π΅ β (Filβπ)) |
12 | 10, 11 | sylancom 589 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β π΅ β (Filβπ)) |
13 | 3 | mopntopon 23808 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
14 | 10, 13 | syl 17 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β π½ β (TopOnβπ)) |
15 | | fmcncfil.2 |
. . . . . . . . 9
β’ πΎ = (MetOpenβπΈ) |
16 | 15 | mopntopon 23808 |
. . . . . . . 8
β’ (πΈ β (βMetβπ) β πΎ β (TopOnβπ)) |
17 | 1, 16 | syl 17 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β πΎ β (TopOnβπ)) |
18 | | simpl3 1194 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β πΉ β (π½ Cn πΎ)) |
19 | | cnflf 23369 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
20 | 19 | simplbda 501 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)) |
21 | 14, 17, 18, 20 | syl21anc 837 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)) |
22 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π΅ β (π½ fLim π) = (π½ fLim π΅)) |
23 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π΅ β (πΎ fLimf π) = (πΎ fLimf π΅)) |
24 | 23 | fveq1d 6849 |
. . . . . . . . 9
β’ (π = π΅ β ((πΎ fLimf π)βπΉ) = ((πΎ fLimf π΅)βπΉ)) |
25 | 24 | eleq2d 2824 |
. . . . . . . 8
β’ (π = π΅ β ((πΉβπ₯) β ((πΎ fLimf π)βπΉ) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) |
26 | 22, 25 | raleqbidv 3322 |
. . . . . . 7
β’ (π = π΅ β (βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ) β βπ₯ β (π½ fLim π΅)(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) |
27 | 26 | rspcv 3580 |
. . . . . 6
β’ (π΅ β (Filβπ) β (βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ) β βπ₯ β (π½ fLim π΅)(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) |
28 | 12, 21, 27 | sylc 65 |
. . . . 5
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β βπ₯ β (π½ fLim π΅)(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ)) |
29 | | df-ral 3066 |
. . . . 5
β’
(βπ₯ β
(π½ fLim π΅)(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ) β βπ₯(π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) |
30 | 28, 29 | sylib 217 |
. . . 4
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β βπ₯(π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) |
31 | | 19.29r 1878 |
. . . . 5
β’
((βπ₯ π₯ β (π½ fLim π΅) β§ βπ₯(π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) β βπ₯(π₯ β (π½ fLim π΅) β§ (π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ)))) |
32 | | pm3.35 802 |
. . . . . 6
β’ ((π₯ β (π½ fLim π΅) β§ (π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ)) |
33 | 32 | eximi 1838 |
. . . . 5
β’
(βπ₯(π₯ β (π½ fLim π΅) β§ (π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) β βπ₯(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ)) |
34 | 31, 33 | syl 17 |
. . . 4
β’
((βπ₯ π₯ β (π½ fLim π΅) β§ βπ₯(π₯ β (π½ fLim π΅) β (πΉβπ₯) β ((πΎ fLimf π΅)βπΉ))) β βπ₯(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ)) |
35 | 7, 30, 34 | syl2anc 585 |
. . 3
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β βπ₯(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ)) |
36 | 3, 15 | metcn 23915 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯π·π¦) < π β ((πΉβπ₯)πΈ(πΉβπ¦)) < π)))) |
37 | 36 | biimpa 478 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯π·π¦) < π β ((πΉβπ₯)πΈ(πΉβπ¦)) < π))) |
38 | 10, 1, 18, 37 | syl21anc 837 |
. . . . . . 7
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β (πΉ:πβΆπ β§ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((π₯π·π¦) < π β ((πΉβπ₯)πΈ(πΉβπ¦)) < π))) |
39 | 38 | simpld 496 |
. . . . . 6
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β πΉ:πβΆπ) |
40 | | flfval 23357 |
. . . . . 6
β’ ((πΎ β (TopOnβπ) β§ π΅ β (Filβπ) β§ πΉ:πβΆπ) β ((πΎ fLimf π΅)βπΉ) = (πΎ fLim ((π FilMap πΉ)βπ΅))) |
41 | 17, 12, 39, 40 | syl3anc 1372 |
. . . . 5
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β ((πΎ fLimf π΅)βπΉ) = (πΎ fLim ((π FilMap πΉ)βπ΅))) |
42 | 41 | eleq2d 2824 |
. . . 4
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β ((πΉβπ₯) β ((πΎ fLimf π΅)βπΉ) β (πΉβπ₯) β (πΎ fLim ((π FilMap πΉ)βπ΅)))) |
43 | 42 | exbidv 1925 |
. . 3
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β (βπ₯(πΉβπ₯) β ((πΎ fLimf π΅)βπΉ) β βπ₯(πΉβπ₯) β (πΎ fLim ((π FilMap πΉ)βπ΅)))) |
44 | 35, 43 | mpbid 231 |
. 2
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β βπ₯(πΉβπ₯) β (πΎ fLim ((π FilMap πΉ)βπ΅))) |
45 | 15 | flimcfil 24694 |
. . . 4
β’ ((πΈ β (βMetβπ) β§ (πΉβπ₯) β (πΎ fLim ((π FilMap πΉ)βπ΅))) β ((π FilMap πΉ)βπ΅) β (CauFilβπΈ)) |
46 | 45 | ex 414 |
. . 3
β’ (πΈ β (βMetβπ) β ((πΉβπ₯) β (πΎ fLim ((π FilMap πΉ)βπ΅)) β ((π FilMap πΉ)βπ΅) β (CauFilβπΈ))) |
47 | 46 | exlimdv 1937 |
. 2
β’ (πΈ β (βMetβπ) β (βπ₯(πΉβπ₯) β (πΎ fLim ((π FilMap πΉ)βπ΅)) β ((π FilMap πΉ)βπ΅) β (CauFilβπΈ))) |
48 | 1, 44, 47 | sylc 65 |
1
β’ (((π· β (CMetβπ) β§ πΈ β (βMetβπ) β§ πΉ β (π½ Cn πΎ)) β§ π΅ β (CauFilβπ·)) β ((π FilMap πΉ)βπ΅) β (CauFilβπΈ)) |