Step | Hyp | Ref
| Expression |
1 | | methaus.1 |
. . 3
⊢ 𝐽 = (MetOpen‘𝐷) |
2 | 1 | mopntop 22245 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
3 | 1 | mopnuni 22246 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
4 | 3 | eleq2d 2687 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽)) |
5 | 4 | biimpar 502 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ ∪ 𝐽) → 𝑥 ∈ 𝑋) |
6 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝐷 ∈ (∞Met‘𝑋)) |
7 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ 𝑋) |
8 | | nnrp 11842 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
9 | 8 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
10 | 9 | rpreccld 11882 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ+) |
11 | 10 | rpxrd 11873 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ*) |
12 | 1 | blopn 22305 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (1 / 𝑛) ∈ ℝ*) → (𝑥(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽) |
13 | 6, 7, 11, 12 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑛 ∈ ℕ) → (𝑥(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽) |
14 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) = (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) |
15 | 13, 14 | fmptd 6385 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ⟶𝐽) |
16 | | frn 6053 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ⟶𝐽 → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ⊆ 𝐽) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ⊆ 𝐽) |
18 | | nnex 11026 |
. . . . . . . . 9
⊢ ℕ
∈ V |
19 | 18 | mptex 6486 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ V |
20 | 19 | rnex 7100 |
. . . . . . 7
⊢ ran
(𝑛 ∈ ℕ ↦
(𝑥(ball‘𝐷)(1 / 𝑛))) ∈ V |
21 | 20 | elpw 4164 |
. . . . . 6
⊢ (ran
(𝑛 ∈ ℕ ↦
(𝑥(ball‘𝐷)(1 / 𝑛))) ∈ 𝒫 𝐽 ↔ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ⊆ 𝐽) |
22 | 17, 21 | sylibr 224 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ∈ 𝒫 𝐽) |
23 | | omelon 8543 |
. . . . . . . . 9
⊢ ω
∈ On |
24 | | nnenom 12779 |
. . . . . . . . . 10
⊢ ℕ
≈ ω |
25 | 24 | ensymi 8006 |
. . . . . . . . 9
⊢ ω
≈ ℕ |
26 | | isnumi 8772 |
. . . . . . . . 9
⊢ ((ω
∈ On ∧ ω ≈ ℕ) → ℕ ∈ dom
card) |
27 | 23, 25, 26 | mp2an 708 |
. . . . . . . 8
⊢ ℕ
∈ dom card |
28 | | ovex 6678 |
. . . . . . . . . 10
⊢ (𝑥(ball‘𝐷)(1 / 𝑛)) ∈ V |
29 | 28, 14 | fnmpti 6022 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) Fn ℕ |
30 | | dffn4 6121 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) Fn ℕ ↔ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ–onto→ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))) |
31 | 29, 30 | mpbi 220 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ–onto→ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) |
32 | | fodomnum 8880 |
. . . . . . . 8
⊢ (ℕ
∈ dom card → ((𝑛
∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))):ℕ–onto→ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ℕ)) |
33 | 27, 31, 32 | mp2 9 |
. . . . . . 7
⊢ ran
(𝑛 ∈ ℕ ↦
(𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ℕ |
34 | | domentr 8015 |
. . . . . . 7
⊢ ((ran
(𝑛 ∈ ℕ ↦
(𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ℕ ∧ ℕ ≈
ω) → ran (𝑛
∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω) |
35 | 33, 24, 34 | mp2an 708 |
. . . . . 6
⊢ ran
(𝑛 ∈ ℕ ↦
(𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω |
36 | 35 | a1i 11 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω) |
37 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → 𝐷 ∈ (∞Met‘𝑋)) |
38 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝐽) |
39 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → 𝑥 ∈ 𝑧) |
40 | 1 | mopni2 22298 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧) |
41 | 37, 38, 39, 40 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧) |
42 | | simp-4l 806 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝐷 ∈ (∞Met‘𝑋)) |
43 | | simp-4r 807 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑥 ∈ 𝑋) |
44 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑦 ∈ ℕ) |
45 | 44 | nnrpd 11870 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑦 ∈ ℝ+) |
46 | 45 | rpreccld 11882 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ∈
ℝ+) |
47 | | blcntr 22218 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (1 / 𝑦) ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦))) |
48 | 42, 43, 46, 47 | syl3anc 1326 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦))) |
49 | 46 | rpxrd 11873 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ∈
ℝ*) |
50 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑟 ∈ ℝ+) |
51 | 50 | rpxrd 11873 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑟 ∈ ℝ*) |
52 | | nnrecre 11057 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (1 /
𝑦) ∈
ℝ) |
53 | 52 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ∈ ℝ) |
54 | 50 | rpred 11872 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → 𝑟 ∈ ℝ) |
55 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) < 𝑟) |
56 | 53, 54, 55 | ltled 10185 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (1 / 𝑦) ≤ 𝑟) |
57 | | ssbl 22228 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ ((1 / 𝑦) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
∧ (1 / 𝑦) ≤ 𝑟) → (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ (𝑥(ball‘𝐷)𝑟)) |
58 | 42, 43, 49, 51, 56, 57 | syl221anc 1337 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ (𝑥(ball‘𝐷)𝑟)) |
59 | | simplrr 801 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧) |
60 | 58, 59 | sstrd 3613 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧) |
61 | 48, 60 | jca 554 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(∞Met‘𝑋) ∧
𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) ∧ (𝑦 ∈ ℕ ∧ (1 / 𝑦) < 𝑟)) → (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)) |
62 | | elrp 11834 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
↔ (𝑟 ∈ ℝ
∧ 0 < 𝑟)) |
63 | | nnrecl 11290 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℝ ∧ 0 <
𝑟) → ∃𝑦 ∈ ℕ (1 / 𝑦) < 𝑟) |
64 | 62, 63 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ ∃𝑦 ∈
ℕ (1 / 𝑦) < 𝑟) |
65 | 64 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) → ∃𝑦 ∈ ℕ (1 / 𝑦) < 𝑟) |
66 | 61, 65 | reximddv 3018 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑧)) → ∃𝑦 ∈ ℕ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)) |
67 | 41, 66 | rexlimddv 3035 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → ∃𝑦 ∈ ℕ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)) |
68 | | ovexd 6680 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ 𝑦 ∈ ℕ) → (𝑥(ball‘𝐷)(1 / 𝑦)) ∈ V) |
69 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑤 ∈ V |
70 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → (1 / 𝑛) = (1 / 𝑦)) |
71 | 70 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑦 → (𝑥(ball‘𝐷)(1 / 𝑛)) = (𝑥(ball‘𝐷)(1 / 𝑦))) |
72 | 71 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) = (𝑦 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑦))) |
73 | 72 | elrnmpt 5372 |
. . . . . . . . . 10
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ↔ ∃𝑦 ∈ ℕ 𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)))) |
74 | 69, 73 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → (𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ↔ ∃𝑦 ∈ ℕ 𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)))) |
75 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)))) |
76 | | sseq1 3626 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)) → (𝑤 ⊆ 𝑧 ↔ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧)) |
77 | 75, 76 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦)) → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))) |
78 | 77 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) ∧ 𝑤 = (𝑥(ball‘𝐷)(1 / 𝑦))) → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))) |
79 | 68, 74, 78 | rexxfr2d 4883 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → (∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑦 ∈ ℕ (𝑥 ∈ (𝑥(ball‘𝐷)(1 / 𝑦)) ∧ (𝑥(ball‘𝐷)(1 / 𝑦)) ⊆ 𝑧))) |
80 | 67, 79 | mpbird 247 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ (𝑧 ∈ 𝐽 ∧ 𝑥 ∈ 𝑧)) → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) |
81 | 80 | expr 643 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) ∧ 𝑧 ∈ 𝐽) → (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
82 | 81 | ralrimiva 2966 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
83 | | breq1 4656 |
. . . . . . 7
⊢ (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → (𝑦 ≼ ω ↔ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω)) |
84 | | rexeq 3139 |
. . . . . . . . 9
⊢ (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) |
85 | 84 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
86 | 85 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → (∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
87 | 83, 86 | anbi12d 747 |
. . . . . 6
⊢ (𝑦 = ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
88 | 87 | rspcev 3309 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℕ ↦
(𝑥(ball‘𝐷)(1 / 𝑛))) ∈ 𝒫 𝐽 ∧ (ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛))) ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ ran (𝑛 ∈ ℕ ↦ (𝑥(ball‘𝐷)(1 / 𝑛)))(𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
89 | 22, 36, 82, 88 | syl12anc 1324 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
90 | 5, 89 | syldan 487 |
. . 3
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ ∪ 𝐽) → ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
91 | 90 | ralrimiva 2966 |
. 2
⊢ (𝐷 ∈ (∞Met‘𝑋) → ∀𝑥 ∈ ∪ 𝐽∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) |
92 | | eqid 2622 |
. . 3
⊢ ∪ 𝐽 =
∪ 𝐽 |
93 | 92 | is1stc2 21245 |
. 2
⊢ (𝐽 ∈ 1st𝜔
↔ (𝐽 ∈ Top ∧
∀𝑥 ∈ ∪ 𝐽∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) |
94 | 2, 91, 93 | sylanbrc 698 |
1
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈
1st𝜔) |