Step | Hyp | Ref
| Expression |
1 | | prdsxms.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ Fin) |
2 | | topnfn 15909 |
. . . . 5
⊢ TopOpen
Fn V |
3 | | prdsxms.r |
. . . . . . 7
⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp) |
4 | | ffn 5958 |
. . . . . . 7
⊢ (𝑅:𝐼⟶∞MetSp → 𝑅 Fn 𝐼) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) |
6 | | dffn2 5960 |
. . . . . 6
⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V) |
7 | 5, 6 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝑅:𝐼⟶V) |
8 | | fnfco 5982 |
. . . . 5
⊢ ((TopOpen
Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen
∘ 𝑅) Fn 𝐼) |
9 | 2, 7, 8 | sylancr 694 |
. . . 4
⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼) |
10 | | prdsxms.c |
. . . . 5
⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))} |
11 | 10 | ptval 21183 |
. . . 4
⊢ ((𝐼 ∈ Fin ∧ (TopOpen
∘ 𝑅) Fn 𝐼) →
(∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶)) |
12 | 1, 9, 11 | syl2anc 691 |
. . 3
⊢ (𝜑 →
(∏t‘(TopOpen ∘ 𝑅)) = (topGen‘𝐶)) |
13 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) ↔
(𝑥 ∈ ran
(ball‘𝐷) ∧ 𝑥 ≠ ∅)) |
14 | | prdsxms.y |
. . . . . . . . . . . 12
⊢ 𝑌 = (𝑆Xs𝑅) |
15 | | prdsxms.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
16 | | prdsxms.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (dist‘𝑌) |
17 | | prdsxms.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑌) |
18 | 14, 15, 1, 16, 17, 3 | prdsxmslem1 22143 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) |
19 | | blrn 22024 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘𝐵) → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) ↔ ∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟))) |
21 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝐷 ∈ (∞Met‘𝐵)) |
22 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑝 ∈ 𝐵) |
23 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → 𝑟 ∈
ℝ*) |
24 | | xbln0 22029 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
25 | 21, 22, 23, 24 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ ↔ 0 < 𝑟)) |
26 | 1 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝐼 ∈ Fin) |
27 | | mptexg 6389 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ Fin → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V) |
29 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V |
30 | 29 | rgenw 2908 |
. . . . . . . . . . . . . . . . . 18
⊢
∀𝑛 ∈
𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) |
32 | 31 | fnmpt 5933 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
𝐼 ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) ∈ V → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼) |
33 | 30, 32 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼) |
34 | 3 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑅:𝐼⟶∞MetSp) |
35 | 34 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp) |
36 | | prdsxms.v |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑉 = (Base‘(𝑅‘𝑘)) |
37 | | prdsxms.e |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉)) |
38 | 36, 37 | xmsxmet 22071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐸 ∈ (∞Met‘𝑉)) |
39 | 35, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
40 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) |
41 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) |
42 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑆 ∈ 𝑊) |
43 | 35 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → ∀𝑘 ∈ 𝐼 (𝑅‘𝑘) ∈ ∞MetSp) |
44 | | simp2l 1080 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑝 ∈ 𝐵) |
45 | 34 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑅 = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) |
46 | 45 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) |
47 | 14, 46 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑌 = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
49 | 17, 48 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
50 | 44, 49 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
51 | 40, 41, 42, 26, 43, 36, 50 | prdsbascl 15966 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → ∀𝑘 ∈ 𝐼 (𝑝‘𝑘) ∈ 𝑉) |
52 | 51 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → (𝑝‘𝑘) ∈ 𝑉) |
53 | | simp2r 1081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑟 ∈
ℝ*) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → 𝑟 ∈ ℝ*) |
55 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(MetOpen‘𝐸) =
(MetOpen‘𝐸) |
56 | 55 | blopn 22115 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑝‘𝑘) ∈ 𝑉 ∧ 𝑟 ∈ ℝ*) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸)) |
57 | 39, 52, 54, 56 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ (MetOpen‘𝐸)) |
58 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑘 → (𝑅‘𝑛) = (𝑅‘𝑘)) |
59 | 58 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑘 → (dist‘(𝑅‘𝑛)) = (dist‘(𝑅‘𝑘))) |
60 | 58 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = (Base‘(𝑅‘𝑘))) |
61 | 60, 36 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑘 → (Base‘(𝑅‘𝑛)) = 𝑉) |
62 | 61 | sqxpeqd 5065 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑘 → ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))) = (𝑉 × 𝑉)) |
63 | 59, 62 | reseq12d 5318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))) |
64 | 63, 37 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑘 → ((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))) = 𝐸) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → (ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛))))) = (ball‘𝐸)) |
66 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → (𝑝‘𝑛) = (𝑝‘𝑘)) |
67 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑘 → 𝑟 = 𝑟) |
68 | 65, 66, 67 | oveq123d 6570 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑘 → ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟) = ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
69 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ∈ V |
70 | 68, 31, 69 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐼 → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
72 | | fvco3 6185 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) |
73 | | prdsxms.k |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘)) |
74 | 72, 73 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅:𝐼⟶∞MetSp ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾) |
75 | 34, 74 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾) |
76 | 73, 36, 37 | xmstopn 22066 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅‘𝑘) ∈ ∞MetSp → 𝐾 = (MetOpen‘𝐸)) |
77 | 35, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸)) |
78 | 75, 77 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (MetOpen‘𝐸)) |
79 | 57, 71, 78 | 3eltr4d 2703 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) ∧ 𝑘 ∈ 𝐼) → ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) |
80 | 79 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) |
81 | 34 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑅 = (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))) |
82 | 81 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑆Xs𝑅) = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) |
83 | 14, 82 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑌 = (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (dist‘𝑌) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))) |
85 | 16, 84 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝐷 = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))) |
86 | 85 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (ball‘𝐷) =
(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))) |
87 | 86 | oveqd 6566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑝(ball‘𝐷)𝑟) = (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟)) |
88 | 58 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)) = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)) |
89 | 88 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) |
91 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) = (dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))) |
92 | 83 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (Base‘𝑌) = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))) |
93 | 17, 92 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝐵 = (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))) |
94 | 44, 93 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 𝑝 ∈ (Base‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛))))) |
95 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → 0 < 𝑟) |
96 | 89, 90, 36, 37, 91, 42, 26, 35, 39, 94, 53, 95 | prdsbl 22106 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑝(ball‘(dist‘(𝑆Xs(𝑛 ∈ 𝐼 ↦ (𝑅‘𝑛)))))𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
97 | 87, 96 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
98 | | fneq1 5893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (𝑔 Fn 𝐼 ↔ (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼)) |
99 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (𝑔‘𝑘) = ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘)) |
100 | 99 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))) |
101 | 100 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘))) |
102 | 98, 101 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))) |
103 | 99, 70 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∧ 𝑘 ∈ 𝐼) → (𝑔‘𝑘) = ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
104 | 103 | ixpeq2dva 7809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → X𝑘 ∈ 𝐼 (𝑔‘𝑘) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
105 | 104 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → ((𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))) |
106 | 102, 105 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = (𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ (((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)))) |
107 | 106 | spcegv 3267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V → ((((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
108 | 107 | 3impib 1254 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) ∈ V ∧ ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟)) Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 ((𝑛 ∈ 𝐼 ↦ ((𝑝‘𝑛)(ball‘((dist‘(𝑅‘𝑛)) ↾ ((Base‘(𝑅‘𝑛)) × (Base‘(𝑅‘𝑛)))))𝑟))‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))) |
109 | 28, 33, 80, 97, 108 | syl121anc 1323 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) ∧ 0 <
𝑟) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))) |
110 | 109 | 3expia 1259 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (0 <
𝑟 → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
111 | 25, 110 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
112 | 111 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → ((𝑝(ball‘𝐷)𝑟) ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
113 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → 𝑥 = (𝑝(ball‘𝐷)𝑟)) |
114 | 113 | neeq1d 2841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ ↔ (𝑝(ball‘𝐷)𝑟) ≠ ∅)) |
115 | | ral0 4028 |
. . . . . . . . . . . . . . . . . . 19
⊢
∀𝑘 ∈
∅ (𝑔‘𝑘) = ∪
((TopOpen ∘ 𝑅)‘𝑘) |
116 | | difeq2 3684 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = (𝐼 ∖ 𝐼)) |
117 | | difid 3902 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∖ 𝐼) = ∅ |
118 | 116, 117 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝐼 → (𝐼 ∖ 𝑧) = ∅) |
119 | 118 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝐼 → (∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘))) |
120 | 119 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ Fin ∧ ∀𝑘 ∈ ∅ (𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
121 | 1, 115, 120 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) →
∃𝑧 ∈ Fin
∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
123 | 122 | biantrud 527 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)))) |
124 | | df-3an 1033 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘))) |
125 | 123, 124 | syl6rbbr 278 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ↔ (𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)))) |
126 | | eqeq1 2614 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘) ↔ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘))) |
127 | 125, 126 | bi2anan9 913 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
128 | 127 | exbidv 1837 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
129 | 112, 114,
128 | 3imtr4d 282 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) ∧ 𝑥 = (𝑝(ball‘𝐷)𝑟)) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
130 | 129 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*)) → (𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))) |
131 | 130 | rexlimdvva 3020 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑝 ∈ 𝐵 ∃𝑟 ∈ ℝ* 𝑥 = (𝑝(ball‘𝐷)𝑟) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))) |
132 | 20, 131 | sylbid 229 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ran (ball‘𝐷) → (𝑥 ≠ ∅ → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))))) |
133 | 132 | impd 446 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ ran (ball‘𝐷) ∧ 𝑥 ≠ ∅) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
134 | 13, 133 | syl5bi 231 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
135 | 134 | alrimiv 1842 |
. . . . . 6
⊢ (𝜑 → ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
136 | | ssab 3635 |
. . . . . 6
⊢ ((ran
(ball‘𝐷) ∖
{∅}) ⊆ {𝑥
∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))} ↔ ∀𝑥(𝑥 ∈ (ran (ball‘𝐷) ∖ {∅}) → ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘)))) |
137 | 135, 136 | sylibr 223 |
. . . . 5
⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆
{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}) |
138 | 137, 10 | syl6sseqr 3615 |
. . . 4
⊢ (𝜑 → (ran (ball‘𝐷) ∖ {∅}) ⊆
𝐶) |
139 | | ssv 3588 |
. . . . . . . . . 10
⊢
∞MetSp ⊆ V |
140 | | fnssres 5918 |
. . . . . . . . . 10
⊢ ((TopOpen
Fn V ∧ ∞MetSp ⊆ V) → (TopOpen ↾ ∞MetSp) Fn
∞MetSp) |
141 | 2, 139, 140 | mp2an 704 |
. . . . . . . . 9
⊢ (TopOpen
↾ ∞MetSp) Fn ∞MetSp |
142 | | fvres 6117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∞MetSp →
((TopOpen ↾ ∞MetSp)‘𝑥) = (TopOpen‘𝑥)) |
143 | | xmstps 22068 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∞MetSp →
𝑥 ∈
TopSp) |
144 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘𝑥) =
(TopOpen‘𝑥) |
145 | 144 | tpstop 20554 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ TopSp →
(TopOpen‘𝑥) ∈
Top) |
146 | 143, 145 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∞MetSp →
(TopOpen‘𝑥) ∈
Top) |
147 | 142, 146 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ∞MetSp →
((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top) |
148 | 147 | rgen 2906 |
. . . . . . . . 9
⊢
∀𝑥 ∈
∞MetSp ((TopOpen ↾ ∞MetSp)‘𝑥) ∈ Top |
149 | | ffnfv 6295 |
. . . . . . . . 9
⊢ ((TopOpen
↾ ∞MetSp):∞MetSp⟶Top ↔ ((TopOpen ↾
∞MetSp) Fn ∞MetSp ∧ ∀𝑥 ∈ ∞MetSp ((TopOpen ↾
∞MetSp)‘𝑥)
∈ Top)) |
150 | 141, 148,
149 | mpbir2an 957 |
. . . . . . . 8
⊢ (TopOpen
↾ ∞MetSp):∞MetSp⟶Top |
151 | | fco2 5972 |
. . . . . . . 8
⊢
(((TopOpen ↾ ∞MetSp):∞MetSp⟶Top ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen
∘ 𝑅):𝐼⟶Top) |
152 | 150, 3, 151 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) |
153 | | eqid 2610 |
. . . . . . . 8
⊢ X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) = X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) |
154 | 10, 153 | ptbasfi 21194 |
. . . . . . 7
⊢ ((𝐼 ∈ Fin ∧ (TopOpen
∘ 𝑅):𝐼⟶Top) → 𝐶 = (fi‘({X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))))) |
155 | 1, 152, 154 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝐶 = (fi‘({X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))))) |
156 | | eqid 2610 |
. . . . . . . . 9
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
157 | 156 | mopntop 22055 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ Top) |
158 | 18, 157 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (MetOpen‘𝐷) ∈ Top) |
159 | 14, 17, 15, 1, 5 | prdsbas2 15952 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 (Base‘(𝑅‘𝑘))) |
160 | 3, 74 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = 𝐾) |
161 | 3 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ ∞MetSp) |
162 | | xmstps 22068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅‘𝑘) ∈ ∞MetSp → (𝑅‘𝑘) ∈ TopSp) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopSp) |
164 | 36, 73 | istps 20551 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅‘𝑘) ∈ TopSp ↔ 𝐾 ∈ (TopOn‘𝑉)) |
165 | 163, 164 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 ∈ (TopOn‘𝑉)) |
166 | 160, 165 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉)) |
167 | | toponuni 20542 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen ∘ 𝑅)‘𝑘) ∈ (TopOn‘𝑉) → 𝑉 = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑉 = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
169 | 36, 168 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘(𝑅‘𝑘)) = ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
170 | 169 | ixpeq2dva 7809 |
. . . . . . . . . . . 12
⊢ (𝜑 → X𝑘 ∈
𝐼 (Base‘(𝑅‘𝑘)) = X𝑘 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
171 | 159, 170 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = X𝑘 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑘)) |
172 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑛)) |
173 | 172 | unieqd 4382 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ∪
((TopOpen ∘ 𝑅)‘𝑘) = ∪ ((TopOpen
∘ 𝑅)‘𝑛)) |
174 | 173 | cbvixpv 7812 |
. . . . . . . . . . 11
⊢ X𝑘 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑘) = X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) |
175 | 171, 174 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛)) |
176 | 156 | mopntopon 22054 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) ∈ (TopOn‘𝐵)) |
177 | 18, 176 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (MetOpen‘𝐷) ∈ (TopOn‘𝐵)) |
178 | | toponmax 20543 |
. . . . . . . . . . 11
⊢
((MetOpen‘𝐷)
∈ (TopOn‘𝐵)
→ 𝐵 ∈
(MetOpen‘𝐷)) |
179 | 177, 178 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (MetOpen‘𝐷)) |
180 | 175, 179 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (𝜑 → X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛) ∈ (MetOpen‘𝐷)) |
181 | 180 | snssd 4281 |
. . . . . . . 8
⊢ (𝜑 → {X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ⊆ (MetOpen‘𝐷)) |
182 | 175 | mpteq1d 4666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘))) |
183 | 182 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘))) |
184 | 183 | cnveqd 5220 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘))) |
185 | 184 | imaeq1d 5384 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) |
186 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑝 → (𝑤‘𝑘) = (𝑝‘𝑘)) |
187 | 186 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑝 → ((𝑤‘𝑘) ∈ 𝑢 ↔ (𝑝‘𝑘) ∈ 𝑢)) |
188 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) |
189 | 188 | mptpreima 5545 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢} |
190 | 187, 189 | elrab2 3333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢)) |
191 | 161, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) |
192 | 191 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐸 ∈ (∞Met‘𝑉)) |
193 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ 𝐾) |
194 | 161, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐾 = (MetOpen‘𝐸)) |
195 | 194 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝐾 = (MetOpen‘𝐸)) |
196 | 193, 195 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑢 ∈ (MetOpen‘𝐸)) |
197 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → (𝑝‘𝑘) ∈ 𝑢) |
198 | 55 | mopni2 22108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑢 ∈ (MetOpen‘𝐸) ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢) |
199 | 192, 196,
197, 198 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑟 ∈ ℝ+ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢) |
200 | 18 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝐷 ∈ (∞Met‘𝐵)) |
201 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → 𝑝 ∈ 𝐵) |
202 | 201 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ 𝐵) |
203 | | rpxr 11716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
204 | 203 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ*) |
205 | 156 | blopn 22115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷)) |
206 | 200, 202,
204, 205 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷)) |
207 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+) |
208 | | blcntr 22028 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟)) |
209 | 200, 202,
207, 208 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝑝 ∈ (𝑝(ball‘𝐷)𝑟)) |
210 | | blssm 22033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐷 ∈ (∞Met‘𝐵) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ*) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵) |
211 | 200, 202,
204, 210 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ 𝐵) |
212 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢) |
213 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 𝜑) |
214 | | rpgt0 11720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
215 | 214 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → 0 < 𝑟) |
216 | 213, 202,
204, 215, 97 | syl121anc 1323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) = X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
217 | 216 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑤 ∈ (𝑝(ball‘𝐷)𝑟) ↔ 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟))) |
218 | 217 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑤 ∈ X𝑘 ∈ 𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
219 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝑤 ∈ V |
220 | 219 | elixp 7801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ X𝑘 ∈
𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) ↔ (𝑤 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))) |
221 | 220 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ X𝑘 ∈
𝐼 ((𝑝‘𝑘)(ball‘𝐸)𝑟) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
222 | 218, 221 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → ∀𝑘 ∈ 𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
223 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → 𝑘 ∈ 𝐼) |
224 | | rsp 2913 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑘 ∈
𝐼 (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟) → (𝑘 ∈ 𝐼 → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟))) |
225 | 222, 223,
224 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ ((𝑝‘𝑘)(ball‘𝐸)𝑟)) |
226 | 212, 225 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) ∧ 𝑤 ∈ (𝑝(ball‘𝐷)𝑟)) → (𝑤‘𝑘) ∈ 𝑢) |
227 | 211, 226 | ssrabdv 3644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ {𝑤 ∈ 𝐵 ∣ (𝑤‘𝑘) ∈ 𝑢}) |
228 | 227, 189 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)) |
229 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑝 ∈ 𝑦 ↔ 𝑝 ∈ (𝑝(ball‘𝐷)𝑟))) |
230 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → (𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) |
231 | 229, 230 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑝(ball‘𝐷)𝑟) → ((𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
232 | 231 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝(ball‘𝐷)𝑟) ∈ (MetOpen‘𝐷) ∧ (𝑝 ∈ (𝑝(ball‘𝐷)𝑟) ∧ (𝑝(ball‘𝐷)𝑟) ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) |
233 | 206, 209,
228, 232 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑝‘𝑘)(ball‘𝐸)𝑟) ⊆ 𝑢)) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) |
234 | 199, 233 | rexlimddv 3017 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑢 ∈ 𝐾 ∧ (𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢))) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) |
235 | 234 | expr 641 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((𝑝 ∈ 𝐵 ∧ (𝑝‘𝑘) ∈ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
236 | 190, 235 | syl5bi 231 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) → ∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
237 | 236 | ralrimiv 2948 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢))) |
238 | 158 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (MetOpen‘𝐷) ∈ Top) |
239 | | eltop2 20590 |
. . . . . . . . . . . . . . . . 17
⊢
((MetOpen‘𝐷)
∈ Top → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → ((◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑝 ∈ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)∃𝑦 ∈ (MetOpen‘𝐷)(𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
241 | 237, 240 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ 𝐵 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
242 | 185, 241 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ 𝑢 ∈ 𝐾) → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
243 | 242 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
244 | 160 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ 𝐾 (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷))) |
245 | 243, 244 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
246 | 245 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
247 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((TopOpen ∘ 𝑅)‘𝑘) = ((TopOpen ∘ 𝑅)‘𝑚)) |
248 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑚 → (𝑤‘𝑘) = (𝑤‘𝑚)) |
249 | 248 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚))) |
250 | 249 | cnveqd 5220 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚))) |
251 | 250 | imaeq1d 5384 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) |
252 | 251 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))) |
253 | 247, 252 | raleqbidv 3129 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷))) |
254 | 253 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
255 | 246, 254 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ 𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷)) |
256 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) = (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) |
257 | 256 | fmpt2x 7125 |
. . . . . . . . . 10
⊢
(∀𝑚 ∈
𝐼 ∀𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚)(◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢) ∈ (MetOpen‘𝐷) ↔ (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷)) |
258 | 255, 257 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷)) |
259 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)):∪ 𝑚 ∈ 𝐼 ({𝑚} × ((TopOpen ∘ 𝑅)‘𝑚))⟶(MetOpen‘𝐷) → ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷)) |
260 | 258, 259 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)) ⊆ (MetOpen‘𝐷)) |
261 | 181, 260 | unssd 3751 |
. . . . . . 7
⊢ (𝜑 → ({X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷)) |
262 | | fiss 8213 |
. . . . . . 7
⊢
(((MetOpen‘𝐷)
∈ Top ∧ ({X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢))) ⊆ (MetOpen‘𝐷)) → (fi‘({X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷))) |
263 | 158, 261,
262 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (fi‘({X𝑛 ∈
𝐼 ∪ ((TopOpen ∘ 𝑅)‘𝑛)} ∪ ran (𝑚 ∈ 𝐼, 𝑢 ∈ ((TopOpen ∘ 𝑅)‘𝑚) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝐼 ∪ ((TopOpen
∘ 𝑅)‘𝑛) ↦ (𝑤‘𝑚)) “ 𝑢)))) ⊆ (fi‘(MetOpen‘𝐷))) |
264 | 155, 263 | eqsstrd 3602 |
. . . . 5
⊢ (𝜑 → 𝐶 ⊆ (fi‘(MetOpen‘𝐷))) |
265 | | fitop 20530 |
. . . . . . 7
⊢
((MetOpen‘𝐷)
∈ Top → (fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷)) |
266 | 158, 265 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(fi‘(MetOpen‘𝐷)) = (MetOpen‘𝐷)) |
267 | 156 | mopnval 22053 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝐵) → (MetOpen‘𝐷) = (topGen‘ran
(ball‘𝐷))) |
268 | 18, 267 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘ran
(ball‘𝐷))) |
269 | | tgdif0 20607 |
. . . . . . 7
⊢
(topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘ran
(ball‘𝐷)) |
270 | 268, 269 | syl6eqr 2662 |
. . . . . 6
⊢ (𝜑 → (MetOpen‘𝐷) = (topGen‘(ran
(ball‘𝐷) ∖
{∅}))) |
271 | 266, 270 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 →
(fi‘(MetOpen‘𝐷)) = (topGen‘(ran (ball‘𝐷) ∖
{∅}))) |
272 | 264, 271 | sseqtrd 3604 |
. . . 4
⊢ (𝜑 → 𝐶 ⊆ (topGen‘(ran
(ball‘𝐷) ∖
{∅}))) |
273 | | 2basgen 20605 |
. . . 4
⊢ (((ran
(ball‘𝐷) ∖
{∅}) ⊆ 𝐶 ∧
𝐶 ⊆
(topGen‘(ran (ball‘𝐷) ∖ {∅}))) →
(topGen‘(ran (ball‘𝐷) ∖ {∅})) = (topGen‘𝐶)) |
274 | 138, 272,
273 | syl2anc 691 |
. . 3
⊢ (𝜑 → (topGen‘(ran
(ball‘𝐷) ∖
{∅})) = (topGen‘𝐶)) |
275 | 12, 274 | eqtr4d 2647 |
. 2
⊢ (𝜑 →
(∏t‘(TopOpen ∘ 𝑅)) = (topGen‘(ran (ball‘𝐷) ∖
{∅}))) |
276 | | prdsxms.j |
. . 3
⊢ 𝐽 = (TopOpen‘𝑌) |
277 | 14, 15, 1, 5, 276 | prdstopn 21241 |
. 2
⊢ (𝜑 → 𝐽 = (∏t‘(TopOpen
∘ 𝑅))) |
278 | 275, 277,
270 | 3eqtr4d 2654 |
1
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) |