Step | Hyp | Ref
| Expression |
1 | | prdsxms.i |
. . . 4
β’ (π β πΌ β Fin) |
2 | | topnfn 17371 |
. . . . 5
β’ TopOpen
Fn V |
3 | | prdsxms.r |
. . . . . . 7
β’ (π β π
:πΌβΆβMetSp) |
4 | 3 | ffnd 6719 |
. . . . . 6
β’ (π β π
Fn πΌ) |
5 | | dffn2 6720 |
. . . . . 6
β’ (π
Fn πΌ β π
:πΌβΆV) |
6 | 4, 5 | sylib 217 |
. . . . 5
β’ (π β π
:πΌβΆV) |
7 | | fnfco 6757 |
. . . . 5
β’ ((TopOpen
Fn V β§ π
:πΌβΆV) β (TopOpen
β π
) Fn πΌ) |
8 | 2, 6, 7 | sylancr 588 |
. . . 4
β’ (π β (TopOpen β π
) Fn πΌ) |
9 | | prdsxms.c |
. . . . 5
β’ πΆ = {π₯ β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ))} |
10 | 9 | ptval 23074 |
. . . 4
β’ ((πΌ β Fin β§ (TopOpen
β π
) Fn πΌ) β
(βtβ(TopOpen β π
)) = (topGenβπΆ)) |
11 | 1, 8, 10 | syl2anc 585 |
. . 3
β’ (π β
(βtβ(TopOpen β π
)) = (topGenβπΆ)) |
12 | | eldifsn 4791 |
. . . . . . . 8
β’ (π₯ β (ran (ballβπ·) β {β
}) β
(π₯ β ran
(ballβπ·) β§ π₯ β β
)) |
13 | | prdsxms.y |
. . . . . . . . . . . 12
β’ π = (πXsπ
) |
14 | | prdsxms.s |
. . . . . . . . . . . 12
β’ (π β π β π) |
15 | | prdsxms.d |
. . . . . . . . . . . 12
β’ π· = (distβπ) |
16 | | prdsxms.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ) |
17 | 13, 14, 1, 15, 16, 3 | prdsxmslem1 24037 |
. . . . . . . . . . 11
β’ (π β π· β (βMetβπ΅)) |
18 | | blrn 23915 |
. . . . . . . . . . 11
β’ (π· β (βMetβπ΅) β (π₯ β ran (ballβπ·) β βπ β π΅ βπ β β* π₯ = (π(ballβπ·)π))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β (π₯ β ran (ballβπ·) β βπ β π΅ βπ β β* π₯ = (π(ballβπ·)π))) |
20 | 17 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β*)) β π· β (βMetβπ΅)) |
21 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β*)) β π β π΅) |
22 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β*)) β π β
β*) |
23 | | xbln0 23920 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π β β*) β ((π(ballβπ·)π) β β
β 0 < π)) |
24 | 20, 21, 22, 23 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β β*)) β ((π(ballβπ·)π) β β
β 0 < π)) |
25 | 1 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β πΌ β Fin) |
26 | 25 | mptexd 7226 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β V) |
27 | | ovex 7442 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π) β V |
28 | 27 | rgenw 3066 |
. . . . . . . . . . . . . . . . . 18
β’
βπ β
πΌ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π) β V |
29 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) |
30 | 29 | fnmpt 6691 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
πΌ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π) β V β (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ) |
31 | 28, 30 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ) |
32 | 3 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π
:πΌβΆβMetSp) |
33 | 32 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β (π
βπ) β βMetSp) |
34 | | prdsxms.v |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = (Baseβ(π
βπ)) |
35 | | prdsxms.e |
. . . . . . . . . . . . . . . . . . . . . 22
β’ πΈ = ((distβ(π
βπ)) βΎ (π Γ π)) |
36 | 34, 35 | xmsxmet 23962 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
βπ) β βMetSp β πΈ β (βMetβπ)) |
37 | 33, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β πΈ β (βMetβπ)) |
38 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πXs(π β πΌ β¦ (π
βπ))) = (πXs(π β πΌ β¦ (π
βπ))) |
39 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(Baseβ(πXs(π β πΌ β¦ (π
βπ)))) = (Baseβ(πXs(π β πΌ β¦ (π
βπ)))) |
40 | 14 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π β π) |
41 | 33 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β βπ β πΌ (π
βπ) β βMetSp) |
42 | | simp2l 1200 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π β π΅) |
43 | 32 | feqmptd 6961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π
= (π β πΌ β¦ (π
βπ))) |
44 | 43 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (πXsπ
) = (πXs(π β πΌ β¦ (π
βπ)))) |
45 | 13, 44 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π = (πXs(π β πΌ β¦ (π
βπ)))) |
46 | 45 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (Baseβπ) = (Baseβ(πXs(π β πΌ β¦ (π
βπ))))) |
47 | 16, 46 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π΅ = (Baseβ(πXs(π β πΌ β¦ (π
βπ))))) |
48 | 42, 47 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π β (Baseβ(πXs(π β πΌ β¦ (π
βπ))))) |
49 | 38, 39, 40, 25, 41, 34, 48 | prdsbascl 17429 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β βπ β πΌ (πβπ) β π) |
50 | 49 | r19.21bi 3249 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β (πβπ) β π) |
51 | | simp2r 1201 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π β
β*) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β π β β*) |
53 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(MetOpenβπΈ) =
(MetOpenβπΈ) |
54 | 53 | blopn 24009 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΈ β (βMetβπ) β§ (πβπ) β π β§ π β β*) β ((πβπ)(ballβπΈ)π) β (MetOpenβπΈ)) |
55 | 37, 50, 52, 54 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β ((πβπ)(ballβπΈ)π) β (MetOpenβπΈ)) |
56 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (distβ(π
βπ)) = (distβ(π
βπ))) |
57 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (Baseβ(π
βπ)) = (Baseβ(π
βπ))) |
58 | 57, 34 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β (Baseβ(π
βπ)) = π) |
59 | 58 | sqxpeqd 5709 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ))) = (π Γ π)) |
60 | 56, 59 | reseq12d 5983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))) = ((distβ(π
βπ)) βΎ (π Γ π))) |
61 | 60, 35 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))) = πΈ) |
62 | 61 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ))))) = (ballβπΈ)) |
63 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πβπ) = (πβπ)) |
64 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β π = π) |
65 | 62, 63, 64 | oveq123d 7430 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π) = ((πβπ)(ballβπΈ)π)) |
66 | | ovex 7442 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ)(ballβπΈ)π) β V |
67 | 65, 29, 66 | fvmpt 6999 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΌ β ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) = ((πβπ)(ballβπΈ)π)) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) = ((πβπ)(ballβπΈ)π)) |
69 | | fvco3 6991 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π
:πΌβΆβMetSp β§ π β πΌ) β ((TopOpen β π
)βπ) = (TopOpenβ(π
βπ))) |
70 | | prdsxms.k |
. . . . . . . . . . . . . . . . . . . . . 22
β’ πΎ = (TopOpenβ(π
βπ)) |
71 | 69, 70 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
:πΌβΆβMetSp β§ π β πΌ) β ((TopOpen β π
)βπ) = πΎ) |
72 | 32, 71 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β ((TopOpen β π
)βπ) = πΎ) |
73 | 70, 34, 35 | xmstopn 23957 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
βπ) β βMetSp β πΎ = (MetOpenβπΈ)) |
74 | 33, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β πΎ = (MetOpenβπΈ)) |
75 | 72, 74 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β ((TopOpen β π
)βπ) = (MetOpenβπΈ)) |
76 | 55, 68, 75 | 3eltr4d 2849 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β§ π β πΌ) β ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ)) |
77 | 76 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β βπ β πΌ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ)) |
78 | 32 | feqmptd 6961 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π
= (π β πΌ β¦ (π
βπ))) |
79 | 78 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (πXsπ
) = (πXs(π β πΌ β¦ (π
βπ)))) |
80 | 13, 79 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π = (πXs(π β πΌ β¦ (π
βπ)))) |
81 | 80 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (distβπ) = (distβ(πXs(π β πΌ β¦ (π
βπ))))) |
82 | 15, 81 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π· = (distβ(πXs(π β πΌ β¦ (π
βπ))))) |
83 | 82 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (ballβπ·) =
(ballβ(distβ(πXs(π β πΌ β¦ (π
βπ)))))) |
84 | 83 | oveqd 7426 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (π(ballβπ·)π) = (π(ballβ(distβ(πXs(π β πΌ β¦ (π
βπ)))))π)) |
85 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π
βπ) = (π
βπ)) |
86 | 85 | cbvmptv 5262 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΌ β¦ (π
βπ)) = (π β πΌ β¦ (π
βπ)) |
87 | 86 | oveq2i 7420 |
. . . . . . . . . . . . . . . . . . 19
β’ (πXs(π β πΌ β¦ (π
βπ))) = (πXs(π β πΌ β¦ (π
βπ))) |
88 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(Baseβ(πXs(π β πΌ β¦ (π
βπ)))) = (Baseβ(πXs(π β πΌ β¦ (π
βπ)))) |
89 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(distβ(πXs(π β πΌ β¦ (π
βπ)))) = (distβ(πXs(π β πΌ β¦ (π
βπ)))) |
90 | 80 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (Baseβπ) = (Baseβ(πXs(π β πΌ β¦ (π
βπ))))) |
91 | 16, 90 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π΅ = (Baseβ(πXs(π β πΌ β¦ (π
βπ))))) |
92 | 42, 91 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β π β (Baseβ(πXs(π β πΌ β¦ (π
βπ))))) |
93 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β 0 < π) |
94 | 87, 88, 34, 35, 89, 40, 25, 33, 37, 92, 51, 93 | prdsbl 24000 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (π(ballβ(distβ(πXs(π β πΌ β¦ (π
βπ)))))π) = Xπ β πΌ ((πβπ)(ballβπΈ)π)) |
95 | 84, 94 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β (π(ballβπ·)π) = Xπ β πΌ ((πβπ)(ballβπΈ)π)) |
96 | | fneq1 6641 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β (π Fn πΌ β (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ)) |
97 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β (πβπ) = ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ)) |
98 | 97 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β ((πβπ) β ((TopOpen β π
)βπ) β ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ))) |
99 | 98 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β (βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β βπ β πΌ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ))) |
100 | 96, 99 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ β§ βπ β πΌ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ)))) |
101 | 97, 67 | sylan9eq 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β§ π β πΌ) β (πβπ) = ((πβπ)(ballβπΈ)π)) |
102 | 101 | ixpeq2dva 8906 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β Xπ β πΌ (πβπ) = Xπ β πΌ ((πβπ)(ballβπΈ)π)) |
103 | 102 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β ((π(ballβπ·)π) = Xπ β πΌ (πβπ) β (π(ballβπ·)π) = Xπ β πΌ ((πβπ)(ballβπΈ)π))) |
104 | 100, 103 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β (((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)) β (((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ β§ βπ β πΌ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ ((πβπ)(ballβπΈ)π)))) |
105 | 104 | spcegv 3588 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β V β ((((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ β§ βπ β πΌ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ ((πβπ)(ballβπΈ)π)) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)))) |
106 | 105 | 3impib 1117 |
. . . . . . . . . . . . . . . . 17
β’ (((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) β V β§ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π)) Fn πΌ β§ βπ β πΌ ((π β πΌ β¦ ((πβπ)(ballβ((distβ(π
βπ)) βΎ ((Baseβ(π
βπ)) Γ (Baseβ(π
βπ)))))π))βπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ ((πβπ)(ballβπΈ)π)) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ))) |
107 | 26, 31, 77, 95, 106 | syl121anc 1376 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β*) β§ 0 <
π) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ))) |
108 | 107 | 3expia 1122 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β β*)) β (0 <
π β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)))) |
109 | 24, 108 | sylbid 239 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ π β β*)) β ((π(ballβπ·)π) β β
β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)))) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β*)) β§ π₯ = (π(ballβπ·)π)) β ((π(ballβπ·)π) β β
β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)))) |
111 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β β*)) β§ π₯ = (π(ballβπ·)π)) β π₯ = (π(ballβπ·)π)) |
112 | 111 | neeq1d 3001 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β*)) β§ π₯ = (π(ballβπ·)π)) β (π₯ β β
β (π(ballβπ·)π) β β
)) |
113 | | df-3an 1090 |
. . . . . . . . . . . . . . . 16
β’ ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ))) |
114 | | ral0 4513 |
. . . . . . . . . . . . . . . . . . 19
β’
βπ β
β
(πβπ) = βͺ
((TopOpen β π
)βπ) |
115 | | difeq2 4117 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = πΌ β (πΌ β π§) = (πΌ β πΌ)) |
116 | | difid 4371 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΌ β πΌ) = β
|
117 | 115, 116 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = πΌ β (πΌ β π§) = β
) |
118 | 117 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = πΌ β (βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ) β βπ β β
(πβπ) = βͺ ((TopOpen
β π
)βπ))) |
119 | 118 | rspcev 3613 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΌ β Fin β§ βπ β β
(πβπ) = βͺ ((TopOpen
β π
)βπ)) β βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) |
120 | 1, 114, 119 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π΅ β§ π β β*)) β
βπ§ β Fin
βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) |
122 | 121 | biantrud 533 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ π β β*)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)))) |
123 | 113, 122 | bitr4id 290 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β β*)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β (π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)))) |
124 | | eqeq1 2737 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π(ballβπ·)π) β (π₯ = Xπ β πΌ (πβπ) β (π(ballβπ·)π) = Xπ β πΌ (πβπ))) |
125 | 123, 124 | bi2anan9 638 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β β*)) β§ π₯ = (π(ballβπ·)π)) β (((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)) β ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)))) |
126 | 125 | exbidv 1925 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΅ β§ π β β*)) β§ π₯ = (π(ballβπ·)π)) β (βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ)) β§ (π(ballβπ·)π) = Xπ β πΌ (πβπ)))) |
127 | 110, 112,
126 | 3imtr4d 294 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΅ β§ π β β*)) β§ π₯ = (π(ballβπ·)π)) β (π₯ β β
β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)))) |
128 | 127 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β β*)) β (π₯ = (π(ballβπ·)π) β (π₯ β β
β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ))))) |
129 | 128 | rexlimdvva 3212 |
. . . . . . . . . 10
β’ (π β (βπ β π΅ βπ β β* π₯ = (π(ballβπ·)π) β (π₯ β β
β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ))))) |
130 | 19, 129 | sylbid 239 |
. . . . . . . . 9
β’ (π β (π₯ β ran (ballβπ·) β (π₯ β β
β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ))))) |
131 | 130 | impd 412 |
. . . . . . . 8
β’ (π β ((π₯ β ran (ballβπ·) β§ π₯ β β
) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)))) |
132 | 12, 131 | biimtrid 241 |
. . . . . . 7
β’ (π β (π₯ β (ran (ballβπ·) β {β
}) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)))) |
133 | 132 | alrimiv 1931 |
. . . . . 6
β’ (π β βπ₯(π₯ β (ran (ballβπ·) β {β
}) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)))) |
134 | | ssab 4059 |
. . . . . 6
β’ ((ran
(ballβπ·) β
{β
}) β {π₯
β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ))} β βπ₯(π₯ β (ran (ballβπ·) β {β
}) β βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ)))) |
135 | 133, 134 | sylibr 233 |
. . . . 5
β’ (π β (ran (ballβπ·) β {β
}) β
{π₯ β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π
)βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen
β π
)βπ)) β§ π₯ = Xπ β πΌ (πβπ))}) |
136 | 135, 9 | sseqtrrdi 4034 |
. . . 4
β’ (π β (ran (ballβπ·) β {β
}) β
πΆ) |
137 | | ssv 4007 |
. . . . . . . . . 10
β’
βMetSp β V |
138 | | fnssres 6674 |
. . . . . . . . . 10
β’ ((TopOpen
Fn V β§ βMetSp β V) β (TopOpen βΎ βMetSp) Fn
βMetSp) |
139 | 2, 137, 138 | mp2an 691 |
. . . . . . . . 9
β’ (TopOpen
βΎ βMetSp) Fn βMetSp |
140 | | fvres 6911 |
. . . . . . . . . . 11
β’ (π₯ β βMetSp β
((TopOpen βΎ βMetSp)βπ₯) = (TopOpenβπ₯)) |
141 | | xmstps 23959 |
. . . . . . . . . . . 12
β’ (π₯ β βMetSp β
π₯ β
TopSp) |
142 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(TopOpenβπ₯) =
(TopOpenβπ₯) |
143 | 142 | tpstop 22439 |
. . . . . . . . . . . 12
β’ (π₯ β TopSp β
(TopOpenβπ₯) β
Top) |
144 | 141, 143 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β βMetSp β
(TopOpenβπ₯) β
Top) |
145 | 140, 144 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (π₯ β βMetSp β
((TopOpen βΎ βMetSp)βπ₯) β Top) |
146 | 145 | rgen 3064 |
. . . . . . . . 9
β’
βπ₯ β
βMetSp ((TopOpen βΎ βMetSp)βπ₯) β Top |
147 | | ffnfv 7118 |
. . . . . . . . 9
β’ ((TopOpen
βΎ βMetSp):βMetSpβΆTop β ((TopOpen βΎ
βMetSp) Fn βMetSp β§ βπ₯ β βMetSp ((TopOpen βΎ
βMetSp)βπ₯)
β Top)) |
148 | 139, 146,
147 | mpbir2an 710 |
. . . . . . . 8
β’ (TopOpen
βΎ βMetSp):βMetSpβΆTop |
149 | | fco2 6745 |
. . . . . . . 8
β’
(((TopOpen βΎ βMetSp):βMetSpβΆTop β§ π
:πΌβΆβMetSp) β (TopOpen
β π
):πΌβΆTop) |
150 | 148, 3, 149 | sylancr 588 |
. . . . . . 7
β’ (π β (TopOpen β π
):πΌβΆTop) |
151 | | eqid 2733 |
. . . . . . . 8
β’ Xπ β
πΌ βͺ ((TopOpen β π
)βπ) = Xπ β πΌ βͺ ((TopOpen
β π
)βπ) |
152 | 9, 151 | ptbasfi 23085 |
. . . . . . 7
β’ ((πΌ β Fin β§ (TopOpen
β π
):πΌβΆTop) β πΆ = (fiβ({Xπ β
πΌ βͺ ((TopOpen β π
)βπ)} βͺ ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’))))) |
153 | 1, 150, 152 | syl2anc 585 |
. . . . . 6
β’ (π β πΆ = (fiβ({Xπ β πΌ βͺ ((TopOpen
β π
)βπ)} βͺ ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’))))) |
154 | | eqid 2733 |
. . . . . . . . 9
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
155 | 154 | mopntop 23946 |
. . . . . . . 8
β’ (π· β (βMetβπ΅) β (MetOpenβπ·) β Top) |
156 | 17, 155 | syl 17 |
. . . . . . 7
β’ (π β (MetOpenβπ·) β Top) |
157 | 13, 16, 14, 1, 4 | prdsbas2 17415 |
. . . . . . . . . . . 12
β’ (π β π΅ = Xπ β πΌ (Baseβ(π
βπ))) |
158 | 3, 71 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β πΌ) β ((TopOpen β π
)βπ) = πΎ) |
159 | 3 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΌ) β (π
βπ) β βMetSp) |
160 | | xmstps 23959 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
βπ) β βMetSp β (π
βπ) β TopSp) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β πΌ) β (π
βπ) β TopSp) |
162 | 34, 70 | istps 22436 |
. . . . . . . . . . . . . . . . 17
β’ ((π
βπ) β TopSp β πΎ β (TopOnβπ)) |
163 | 161, 162 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β πΌ) β πΎ β (TopOnβπ)) |
164 | 158, 163 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΌ) β ((TopOpen β π
)βπ) β (TopOnβπ)) |
165 | | toponuni 22416 |
. . . . . . . . . . . . . . 15
β’
(((TopOpen β π
)βπ) β (TopOnβπ) β π = βͺ ((TopOpen
β π
)βπ)) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΌ) β π = βͺ ((TopOpen
β π
)βπ)) |
167 | 34, 166 | eqtr3id 2787 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (Baseβ(π
βπ)) = βͺ ((TopOpen
β π
)βπ)) |
168 | 167 | ixpeq2dva 8906 |
. . . . . . . . . . . 12
β’ (π β Xπ β
πΌ (Baseβ(π
βπ)) = Xπ β πΌ βͺ ((TopOpen
β π
)βπ)) |
169 | 157, 168 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β π΅ = Xπ β πΌ βͺ ((TopOpen
β π
)βπ)) |
170 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β ((TopOpen β π
)βπ) = ((TopOpen β π
)βπ)) |
171 | 170 | unieqd 4923 |
. . . . . . . . . . . 12
β’ (π = π β βͺ
((TopOpen β π
)βπ) = βͺ ((TopOpen
β π
)βπ)) |
172 | 171 | cbvixpv 8909 |
. . . . . . . . . . 11
β’ Xπ β
πΌ βͺ ((TopOpen β π
)βπ) = Xπ β πΌ βͺ ((TopOpen
β π
)βπ) |
173 | 169, 172 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β π΅ = Xπ β πΌ βͺ ((TopOpen
β π
)βπ)) |
174 | 154 | mopntopon 23945 |
. . . . . . . . . . . 12
β’ (π· β (βMetβπ΅) β (MetOpenβπ·) β (TopOnβπ΅)) |
175 | 17, 174 | syl 17 |
. . . . . . . . . . 11
β’ (π β (MetOpenβπ·) β (TopOnβπ΅)) |
176 | | toponmax 22428 |
. . . . . . . . . . 11
β’
((MetOpenβπ·)
β (TopOnβπ΅)
β π΅ β
(MetOpenβπ·)) |
177 | 175, 176 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ β (MetOpenβπ·)) |
178 | 173, 177 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β Xπ β
πΌ βͺ ((TopOpen β π
)βπ) β (MetOpenβπ·)) |
179 | 178 | snssd 4813 |
. . . . . . . 8
β’ (π β {Xπ β
πΌ βͺ ((TopOpen β π
)βπ)} β (MetOpenβπ·)) |
180 | 173 | mpteq1d 5244 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π€ β π΅ β¦ (π€βπ)) = (π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ))) |
181 | 180 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β (π€ β π΅ β¦ (π€βπ)) = (π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ))) |
182 | 181 | cnveqd 5876 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β β‘(π€ β π΅ β¦ (π€βπ)) = β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ))) |
183 | 182 | imaeq1d 6059 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β (β‘(π€ β π΅ β¦ (π€βπ)) β π’) = (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)) |
184 | | fveq1 6891 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π β (π€βπ) = (πβπ)) |
185 | 184 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = π β ((π€βπ) β π’ β (πβπ) β π’)) |
186 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β π΅ β¦ (π€βπ)) = (π€ β π΅ β¦ (π€βπ)) |
187 | 186 | mptpreima 6238 |
. . . . . . . . . . . . . . . . . . 19
β’ (β‘(π€ β π΅ β¦ (π€βπ)) β π’) = {π€ β π΅ β£ (π€βπ) β π’} |
188 | 185, 187 | elrab2 3687 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β‘(π€ β π΅ β¦ (π€βπ)) β π’) β (π β π΅ β§ (πβπ) β π’)) |
189 | 159, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β πΌ) β πΈ β (βMetβπ)) |
190 | 189 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β πΈ β (βMetβπ)) |
191 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β π’ β πΎ) |
192 | 159, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β πΌ) β πΎ = (MetOpenβπΈ)) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β πΎ = (MetOpenβπΈ)) |
194 | 191, 193 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β π’ β (MetOpenβπΈ)) |
195 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β (πβπ) β π’) |
196 | 53 | mopni2 24002 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΈ β (βMetβπ) β§ π’ β (MetOpenβπΈ) β§ (πβπ) β π’) β βπ β β+ ((πβπ)(ballβπΈ)π) β π’) |
197 | 190, 194,
195, 196 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β βπ β β+ ((πβπ)(ballβπΈ)π) β π’) |
198 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β π· β (βMetβπ΅)) |
199 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β π β π΅) |
200 | 199 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β π β π΅) |
201 | | rpxr 12983 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β+
β π β
β*) |
202 | 201 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β π β β*) |
203 | 154 | blopn 24009 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π β β*) β (π(ballβπ·)π) β (MetOpenβπ·)) |
204 | 198, 200,
202, 203 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β (π(ballβπ·)π) β (MetOpenβπ·)) |
205 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β π β β+) |
206 | | blcntr 23919 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π β β+) β π β (π(ballβπ·)π)) |
207 | 198, 200,
205, 206 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β π β (π(ballβπ·)π)) |
208 | | blssm 23924 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π· β (βMetβπ΅) β§ π β π΅ β§ π β β*) β (π(ballβπ·)π) β π΅) |
209 | 198, 200,
202, 208 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β (π(ballβπ·)π) β π΅) |
210 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β§ π€ β (π(ballβπ·)π)) β ((πβπ)(ballβπΈ)π) β π’) |
211 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β π) |
212 | | rpgt0 12986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β+
β 0 < π) |
213 | 212 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β 0 < π) |
214 | 211, 200,
202, 213, 95 | syl121anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β (π(ballβπ·)π) = Xπ β πΌ ((πβπ)(ballβπΈ)π)) |
215 | 214 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β (π€ β (π(ballβπ·)π) β π€ β Xπ β πΌ ((πβπ)(ballβπΈ)π))) |
216 | 215 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β§ π€ β (π(ballβπ·)π)) β π€ β Xπ β πΌ ((πβπ)(ballβπΈ)π)) |
217 | | vex 3479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π€ β V |
218 | 217 | elixp 8898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ β Xπ β
πΌ ((πβπ)(ballβπΈ)π) β (π€ Fn πΌ β§ βπ β πΌ (π€βπ) β ((πβπ)(ballβπΈ)π))) |
219 | 218 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ β Xπ β
πΌ ((πβπ)(ballβπΈ)π) β βπ β πΌ (π€βπ) β ((πβπ)(ballβπΈ)π)) |
220 | 216, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β§ π€ β (π(ballβπ·)π)) β βπ β πΌ (π€βπ) β ((πβπ)(ballβπΈ)π)) |
221 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β§ π€ β (π(ballβπ·)π)) β π β πΌ) |
222 | | rsp 3245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
πΌ (π€βπ) β ((πβπ)(ballβπΈ)π) β (π β πΌ β (π€βπ) β ((πβπ)(ballβπΈ)π))) |
223 | 220, 221,
222 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β§ π€ β (π(ballβπ·)π)) β (π€βπ) β ((πβπ)(ballβπΈ)π)) |
224 | 210, 223 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β§ π€ β (π(ballβπ·)π)) β (π€βπ) β π’) |
225 | 209, 224 | ssrabdv 4072 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β (π(ballβπ·)π) β {π€ β π΅ β£ (π€βπ) β π’}) |
226 | 225, 187 | sseqtrrdi 4034 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β (π(ballβπ·)π) β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)) |
227 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ = (π(ballβπ·)π) β (π β π¦ β π β (π(ballβπ·)π))) |
228 | | sseq1 4008 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ = (π(ballβπ·)π) β (π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’) β (π(ballβπ·)π) β (β‘(π€ β π΅ β¦ (π€βπ)) β π’))) |
229 | 227, 228 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = (π(ballβπ·)π) β ((π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)) β (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)))) |
230 | 229 | rspcev 3613 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π(ballβπ·)π) β (MetOpenβπ·) β§ (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β (β‘(π€ β π΅ β¦ (π€βπ)) β π’))) β βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’))) |
231 | 204, 207,
226, 230 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β§ (π β β+ β§ ((πβπ)(ballβπΈ)π) β π’)) β βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’))) |
232 | 197, 231 | rexlimddv 3162 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β πΌ) β§ (π’ β πΎ β§ (π β π΅ β§ (πβπ) β π’))) β βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’))) |
233 | 232 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β ((π β π΅ β§ (πβπ) β π’) β βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)))) |
234 | 188, 233 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β (π β (β‘(π€ β π΅ β¦ (π€βπ)) β π’) β βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)))) |
235 | 234 | ralrimiv 3146 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β βπ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’))) |
236 | 156 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β (MetOpenβπ·) β Top) |
237 | | eltop2 22478 |
. . . . . . . . . . . . . . . . 17
β’
((MetOpenβπ·)
β Top β ((β‘(π€ β π΅ β¦ (π€βπ)) β π’) β (MetOpenβπ·) β βπ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)))) |
238 | 236, 237 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β ((β‘(π€ β π΅ β¦ (π€βπ)) β π’) β (MetOpenβπ·) β βπ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)βπ¦ β (MetOpenβπ·)(π β π¦ β§ π¦ β (β‘(π€ β π΅ β¦ (π€βπ)) β π’)))) |
239 | 235, 238 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β (β‘(π€ β π΅ β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
240 | 183, 239 | eqeltrrd 2835 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β πΌ) β§ π’ β πΎ) β (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
241 | 240 | ralrimiva 3147 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β βπ’ β πΎ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
242 | 158 | raleqdv 3326 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·) β βπ’ β πΎ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·))) |
243 | 241, 242 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
244 | 243 | ralrimiva 3147 |
. . . . . . . . . . 11
β’ (π β βπ β πΌ βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
245 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β ((TopOpen β π
)βπ) = ((TopOpen β π
)βπ)) |
246 | | fveq2 6892 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π€βπ) = (π€βπ)) |
247 | 246 | mpteq2dv 5251 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) = (π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ))) |
248 | 247 | cnveqd 5876 |
. . . . . . . . . . . . . . 15
β’ (π = π β β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) = β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ))) |
249 | 248 | imaeq1d 6059 |
. . . . . . . . . . . . . 14
β’ (π = π β (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) = (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)) |
250 | 249 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π = π β ((β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·) β (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·))) |
251 | 245, 250 | raleqbidv 3343 |
. . . . . . . . . . . 12
β’ (π = π β (βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·) β βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·))) |
252 | 251 | cbvralvw 3235 |
. . . . . . . . . . 11
β’
(βπ β
πΌ βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·) β βπ β πΌ βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
253 | 244, 252 | sylib 217 |
. . . . . . . . . 10
β’ (π β βπ β πΌ βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·)) |
254 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)) = (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)) |
255 | 254 | fmpox 8053 |
. . . . . . . . . 10
β’
(βπ β
πΌ βπ’ β ((TopOpen β π
)βπ)(β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’) β (MetOpenβπ·) β (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)):βͺ π β πΌ ({π} Γ ((TopOpen β π
)βπ))βΆ(MetOpenβπ·)) |
256 | 253, 255 | sylib 217 |
. . . . . . . . 9
β’ (π β (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)):βͺ π β πΌ ({π} Γ ((TopOpen β π
)βπ))βΆ(MetOpenβπ·)) |
257 | 256 | frnd 6726 |
. . . . . . . 8
β’ (π β ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)) β (MetOpenβπ·)) |
258 | 179, 257 | unssd 4187 |
. . . . . . 7
β’ (π β ({Xπ β
πΌ βͺ ((TopOpen β π
)βπ)} βͺ ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’))) β (MetOpenβπ·)) |
259 | | fiss 9419 |
. . . . . . 7
β’
(((MetOpenβπ·)
β Top β§ ({Xπ β πΌ βͺ ((TopOpen
β π
)βπ)} βͺ ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’))) β (MetOpenβπ·)) β (fiβ({Xπ β
πΌ βͺ ((TopOpen β π
)βπ)} βͺ ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)))) β (fiβ(MetOpenβπ·))) |
260 | 156, 258,
259 | syl2anc 585 |
. . . . . 6
β’ (π β (fiβ({Xπ β
πΌ βͺ ((TopOpen β π
)βπ)} βͺ ran (π β πΌ, π’ β ((TopOpen β π
)βπ) β¦ (β‘(π€ β Xπ β πΌ βͺ ((TopOpen
β π
)βπ) β¦ (π€βπ)) β π’)))) β (fiβ(MetOpenβπ·))) |
261 | 153, 260 | eqsstrd 4021 |
. . . . 5
β’ (π β πΆ β (fiβ(MetOpenβπ·))) |
262 | | fitop 22402 |
. . . . . . 7
β’
((MetOpenβπ·)
β Top β (fiβ(MetOpenβπ·)) = (MetOpenβπ·)) |
263 | 156, 262 | syl 17 |
. . . . . 6
β’ (π β
(fiβ(MetOpenβπ·)) = (MetOpenβπ·)) |
264 | 154 | mopnval 23944 |
. . . . . . . 8
β’ (π· β (βMetβπ΅) β (MetOpenβπ·) = (topGenβran
(ballβπ·))) |
265 | 17, 264 | syl 17 |
. . . . . . 7
β’ (π β (MetOpenβπ·) = (topGenβran
(ballβπ·))) |
266 | | tgdif0 22495 |
. . . . . . 7
β’
(topGenβ(ran (ballβπ·) β {β
})) = (topGenβran
(ballβπ·)) |
267 | 265, 266 | eqtr4di 2791 |
. . . . . 6
β’ (π β (MetOpenβπ·) = (topGenβ(ran
(ballβπ·) β
{β
}))) |
268 | 263, 267 | eqtrd 2773 |
. . . . 5
β’ (π β
(fiβ(MetOpenβπ·)) = (topGenβ(ran (ballβπ·) β
{β
}))) |
269 | 261, 268 | sseqtrd 4023 |
. . . 4
β’ (π β πΆ β (topGenβ(ran
(ballβπ·) β
{β
}))) |
270 | | 2basgen 22493 |
. . . 4
β’ (((ran
(ballβπ·) β
{β
}) β πΆ β§
πΆ β
(topGenβ(ran (ballβπ·) β {β
}))) β
(topGenβ(ran (ballβπ·) β {β
})) = (topGenβπΆ)) |
271 | 136, 269,
270 | syl2anc 585 |
. . 3
β’ (π β (topGenβ(ran
(ballβπ·) β
{β
})) = (topGenβπΆ)) |
272 | 11, 271 | eqtr4d 2776 |
. 2
β’ (π β
(βtβ(TopOpen β π
)) = (topGenβ(ran (ballβπ·) β
{β
}))) |
273 | | prdsxms.j |
. . 3
β’ π½ = (TopOpenβπ) |
274 | 13, 14, 1, 4, 273 | prdstopn 23132 |
. 2
β’ (π β π½ = (βtβ(TopOpen
β π
))) |
275 | 272, 274,
267 | 3eqtr4d 2783 |
1
β’ (π β π½ = (MetOpenβπ·)) |