Step | Hyp | Ref
| Expression |
1 | | qndenserrnopnlem.i |
. . . . 5
β’ (π β πΌ β Fin) |
2 | | qndenserrnopnlem.d |
. . . . . 6
β’ π· =
(distβ(β^βπΌ)) |
3 | 2 | rrxmetfi 24814 |
. . . . 5
β’ (πΌ β Fin β π· β (Metβ(β
βm πΌ))) |
4 | 1, 3 | syl 17 |
. . . 4
β’ (π β π· β (Metβ(β
βm πΌ))) |
5 | | metxmet 23725 |
. . . 4
β’ (π· β (Metβ(β
βm πΌ))
β π· β
(βMetβ(β βm πΌ))) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β π· β (βMetβ(β
βm πΌ))) |
7 | | qndenserrnopnlem.v |
. . . . 5
β’ (π β π β π½) |
8 | | qndenserrnopnlem.j |
. . . . 5
β’ π½ =
(TopOpenβ(β^βπΌ)) |
9 | 7, 8 | eleqtrdi 2843 |
. . . 4
β’ (π β π β (TopOpenβ(β^βπΌ))) |
10 | 1 | rrxtopnfi 44630 |
. . . . 5
β’ (π β
(TopOpenβ(β^βπΌ)) = (MetOpenβ(π β (β βm πΌ), π β (β βm πΌ) β¦
(ββΞ£π
β πΌ (((πβπ) β (πβπ))β2))))) |
11 | 2 | a1i 11 |
. . . . . . 7
β’ (π β π· = (distβ(β^βπΌ))) |
12 | | eqid 2732 |
. . . . . . . . 9
β’
(β^βπΌ) =
(β^βπΌ) |
13 | | eqid 2732 |
. . . . . . . . 9
β’ (β
βm πΌ) =
(β βm πΌ) |
14 | 12, 13 | rrxdsfi 24813 |
. . . . . . . 8
β’ (πΌ β Fin β
(distβ(β^βπΌ)) = (π β (β βm πΌ), π β (β βm πΌ) β¦
(ββΞ£π
β πΌ (((πβπ) β (πβπ))β2)))) |
15 | 1, 14 | syl 17 |
. . . . . . 7
β’ (π β
(distβ(β^βπΌ)) = (π β (β βm πΌ), π β (β βm πΌ) β¦
(ββΞ£π
β πΌ (((πβπ) β (πβπ))β2)))) |
16 | 11, 15 | eqtr2d 2773 |
. . . . . 6
β’ (π β (π β (β βm πΌ), π β (β βm πΌ) β¦
(ββΞ£π
β πΌ (((πβπ) β (πβπ))β2))) = π·) |
17 | 16 | fveq2d 6852 |
. . . . 5
β’ (π β (MetOpenβ(π β (β
βm πΌ),
π β (β
βm πΌ)
β¦ (ββΞ£π β πΌ (((πβπ) β (πβπ))β2)))) = (MetOpenβπ·)) |
18 | 10, 17 | eqtrd 2772 |
. . . 4
β’ (π β
(TopOpenβ(β^βπΌ)) = (MetOpenβπ·)) |
19 | 9, 18 | eleqtrd 2835 |
. . 3
β’ (π β π β (MetOpenβπ·)) |
20 | | qndenserrnopnlem.x |
. . 3
β’ (π β π β π) |
21 | | eqid 2732 |
. . . 4
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
22 | 21 | mopni2 23887 |
. . 3
β’ ((π· β
(βMetβ(β βm πΌ)) β§ π β (MetOpenβπ·) β§ π β π) β βπ β β+ (π(ballβπ·)π) β π) |
23 | 6, 19, 20, 22 | syl3anc 1372 |
. 2
β’ (π β βπ β β+ (π(ballβπ·)π) β π) |
24 | 1 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ π β β+ β§ (π(ballβπ·)π) β π) β πΌ β Fin) |
25 | | rrxtps 44629 |
. . . . . . . . . . . 12
β’ (πΌ β Fin β
(β^βπΌ) β
TopSp) |
26 | 1, 25 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β^βπΌ) β TopSp) |
27 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(Baseβ(β^βπΌ)) = (Baseβ(β^βπΌ)) |
28 | 27, 8 | istps 22321 |
. . . . . . . . . . 11
β’
((β^βπΌ)
β TopSp β π½
β (TopOnβ(Baseβ(β^βπΌ)))) |
29 | 26, 28 | sylib 217 |
. . . . . . . . . 10
β’ (π β π½ β
(TopOnβ(Baseβ(β^βπΌ)))) |
30 | 1, 12, 27 | rrxbasefi 24812 |
. . . . . . . . . . 11
β’ (π β
(Baseβ(β^βπΌ)) = (β βm πΌ)) |
31 | 30 | fveq2d 6852 |
. . . . . . . . . 10
β’ (π β
(TopOnβ(Baseβ(β^βπΌ))) = (TopOnβ(β
βm πΌ))) |
32 | 29, 31 | eleqtrd 2835 |
. . . . . . . . 9
β’ (π β π½ β (TopOnβ(β
βm πΌ))) |
33 | | toponss 22314 |
. . . . . . . . 9
β’ ((π½ β (TopOnβ(β
βm πΌ))
β§ π β π½) β π β (β βm πΌ)) |
34 | 32, 7, 33 | syl2anc 585 |
. . . . . . . 8
β’ (π β π β (β βm πΌ)) |
35 | 34, 20 | sseldd 3949 |
. . . . . . 7
β’ (π β π β (β βm πΌ)) |
36 | 35 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β§ π β β+ β§ (π(ballβπ·)π) β π) β π β (β βm πΌ)) |
37 | | simp2 1138 |
. . . . . 6
β’ ((π β§ π β β+ β§ (π(ballβπ·)π) β π) β π β β+) |
38 | 24, 36, 2, 37 | qndenserrnbl 44638 |
. . . . 5
β’ ((π β§ π β β+ β§ (π(ballβπ·)π) β π) β βπ¦ β (β βm πΌ)π¦ β (π(ballβπ·)π)) |
39 | | ssel 3941 |
. . . . . . . 8
β’ ((π(ballβπ·)π) β π β (π¦ β (π(ballβπ·)π) β π¦ β π)) |
40 | 39 | adantr 482 |
. . . . . . 7
β’ (((π(ballβπ·)π) β π β§ π¦ β (β βm πΌ)) β (π¦ β (π(ballβπ·)π) β π¦ β π)) |
41 | 40 | 3ad2antl3 1188 |
. . . . . 6
β’ (((π β§ π β β+ β§ (π(ballβπ·)π) β π) β§ π¦ β (β βm πΌ)) β (π¦ β (π(ballβπ·)π) β π¦ β π)) |
42 | 41 | reximdva 3162 |
. . . . 5
β’ ((π β§ π β β+ β§ (π(ballβπ·)π) β π) β (βπ¦ β (β βm πΌ)π¦ β (π(ballβπ·)π) β βπ¦ β (β βm πΌ)π¦ β π)) |
43 | 38, 42 | mpd 15 |
. . . 4
β’ ((π β§ π β β+ β§ (π(ballβπ·)π) β π) β βπ¦ β (β βm πΌ)π¦ β π) |
44 | 43 | 3exp 1120 |
. . 3
β’ (π β (π β β+ β ((π(ballβπ·)π) β π β βπ¦ β (β βm πΌ)π¦ β π))) |
45 | 44 | rexlimdv 3147 |
. 2
β’ (π β (βπ β β+ (π(ballβπ·)π) β π β βπ¦ β (β βm πΌ)π¦ β π)) |
46 | 23, 45 | mpd 15 |
1
β’ (π β βπ¦ β (β βm πΌ)π¦ β π) |