Step | Hyp | Ref
| Expression |
1 | | heibor.1 |
. . 3
⊢ 𝐽 = (MetOpen‘𝐷) |
2 | 1 | heibor1 32779 |
. 2
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) |
3 | | cmetmet 22892 |
. . . 4
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
4 | 3 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐷 ∈ (Met‘𝑋)) |
5 | | metxmet 21949 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
6 | 1 | mopntop 22055 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
7 | 3, 5, 6 | 3syl 18 |
. . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐽 ∈ Top) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Top) |
9 | | istotbnd 32738 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)))) |
10 | 9 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ ℝ+
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟))) |
11 | | 2nn 11062 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
12 | | nnexpcl 12735 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
13 | 11, 12 | mpan 702 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (2↑𝑛) ∈
ℕ) |
14 | 13 | nnrpd 11746 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (2↑𝑛) ∈
ℝ+) |
15 | 14 | rpreccld 11758 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (1 / (2↑𝑛))
∈ ℝ+) |
16 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = (1 / (2↑𝑛)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
17 | 16 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = (1 / (2↑𝑛)) → (𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
18 | 17 | rexbidv 3034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = (1 / (2↑𝑛)) → (∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
19 | 18 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = (1 / (2↑𝑛)) → (∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
20 | 19 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = (1 / (2↑𝑛)) → ((∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ (∪ 𝑢 = 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) |
21 | 20 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑟 = (1 / (2↑𝑛)) → (∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ ∃𝑢 ∈ Fin (∪
𝑢 = 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) |
22 | 21 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑟 ∈
ℝ+ ∃𝑢 ∈ Fin (∪
𝑢 = 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ∧ (1 / (2↑𝑛)) ∈ ℝ+) →
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
23 | 10, 15, 22 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (TotBnd‘𝑋) ∧ 𝑛 ∈ ℕ0) →
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
24 | 23 | expcom 450 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝐷 ∈
(TotBnd‘𝑋) →
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) |
25 | 24 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) |
26 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑚‘𝑣) → (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
27 | 26 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑚‘𝑣) → (𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
28 | 27 | ac6sfi 8089 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Fin ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
29 | 28 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
30 | 29 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
31 | | simp3l 1082 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:𝑢⟶𝑋) |
32 | | frn 5966 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚:𝑢⟶𝑋 → ran 𝑚 ⊆ 𝑋) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ⊆ 𝑋) |
34 | 1 | mopnuni 22056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
35 | 3, 5, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 = ∪ 𝐽) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑋 = ∪
𝐽) |
37 | 36 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = ∪ 𝐽) |
38 | 33, 37 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ⊆ ∪ 𝐽) |
39 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(MetOpen‘𝐷)
∈ V |
40 | 1, 39 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 ∈ V |
41 | 40 | uniex 6851 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽
∈ V |
42 | 41 | elpw2 4755 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
𝑚 ∈ 𝒫 ∪ 𝐽
↔ ran 𝑚 ⊆ ∪ 𝐽) |
43 | 38, 42 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ 𝒫 ∪ 𝐽) |
44 | | simp2l 1080 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 ∈ Fin) |
45 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚:𝑢⟶𝑋 → 𝑚 Fn 𝑢) |
46 | | dffn4 6034 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 Fn 𝑢 ↔ 𝑚:𝑢–onto→ran 𝑚) |
47 | 45, 46 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚:𝑢⟶𝑋 → 𝑚:𝑢–onto→ran 𝑚) |
48 | | fofi 8135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ Fin ∧ 𝑚:𝑢–onto→ran 𝑚) → ran 𝑚 ∈ Fin) |
49 | 47, 48 | sylan2 490 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ Fin ∧ 𝑚:𝑢⟶𝑋) → ran 𝑚 ∈ Fin) |
50 | 44, 31, 49 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ Fin) |
51 | 43, 50 | elind 3760 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ (𝒫 ∪ 𝐽
∩ Fin)) |
52 | 26 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑚‘𝑣) → (𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 ∈ ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
53 | 52 | rexrn 6269 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 Fn 𝑢 → (∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣 ∈ 𝑢 𝑟 ∈ ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
54 | | eliun 4460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
55 | | eliun 4460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣 ∈ 𝑢 𝑟 ∈ ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
56 | 53, 54, 55 | 3bitr4g 302 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 Fn 𝑢 → (𝑟 ∈ ∪
𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 ∈ ∪
𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) |
57 | 56 | eqrdv 2608 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 Fn 𝑢 → ∪
𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
58 | 31, 45, 57 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
59 | | simp3r 1083 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
60 | | uniiun 4509 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑢 =
∪ 𝑣 ∈ 𝑢 𝑣 |
61 | | iuneq2 4473 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑣 ∈
𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → ∪ 𝑣 ∈ 𝑢 𝑣 = ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
62 | 60, 61 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑣 ∈
𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → ∪ 𝑢 = ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
63 | 59, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∪
𝑢 = ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) |
64 | | simp2r 1081 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∪
𝑢 = 𝑋) |
65 | 58, 63, 64 | 3eqtr2rd 2651 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
66 | | iuneq1 4470 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = ran 𝑚 → ∪
𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
67 | 66 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = ran 𝑚 → (𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑋 = ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
68 | 67 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ ((ran
𝑚 ∈ (𝒫 ∪ 𝐽
∩ Fin) ∧ 𝑋 =
∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
69 | 51, 65, 68 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
70 | 69 | 3expia 1259 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋)) → ((𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
71 | 70 | adantrrr 757 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ((𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
72 | 71 | exlimdv 1848 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → (∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
73 | 30, 72 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
74 | 73 | rexlimdvaa 3014 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) →
(∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
75 | 25, 74 | syld 46 |
. . . . . . . 8
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
76 | 75 | ralrimdva 2952 |
. . . . . . 7
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑛 ∈ ℕ0 ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
77 | 41 | pwex 4774 |
. . . . . . . . 9
⊢ 𝒫
∪ 𝐽 ∈ V |
78 | 77 | inex1 4727 |
. . . . . . . 8
⊢
(𝒫 ∪ 𝐽 ∩ Fin) ∈ V |
79 | | nn0ennn 12640 |
. . . . . . . . 9
⊢
ℕ0 ≈ ℕ |
80 | | nnenom 12641 |
. . . . . . . . 9
⊢ ℕ
≈ ω |
81 | 79, 80 | entri 7896 |
. . . . . . . 8
⊢
ℕ0 ≈ ω |
82 | | iuneq1 4470 |
. . . . . . . . 9
⊢ (𝑡 = (𝑚‘𝑛) → ∪
𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
83 | 82 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑡 = (𝑚‘𝑛) → (𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
84 | 78, 81, 83 | axcc4 9144 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ0 ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∃𝑚(𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
85 | 76, 84 | syl6 34 |
. . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑚(𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) |
86 | | elpwi 4117 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 𝐽 → 𝑟 ⊆ 𝐽) |
87 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣} = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣} |
88 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
{〈𝑡, 𝑘〉 ∣ (𝑘 ∈ ℕ0
∧ 𝑡 ∈ (𝑚‘𝑘) ∧ (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣})} = {〈𝑡, 𝑘〉 ∣ (𝑘 ∈ ℕ0 ∧ 𝑡 ∈ (𝑚‘𝑘) ∧ (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣})} |
89 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) |
90 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝐷 ∈ (CMet‘𝑋)) |
91 | 35 | pweqd 4113 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝒫 𝑋 = 𝒫 ∪ 𝐽) |
92 | 91 | ineq1d 3775 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝒫 𝑋 ∩ Fin) = (𝒫 ∪ 𝐽
∩ Fin)) |
93 | 92 | feq3d 5945 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin) ↔ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin))) |
94 | 93 | biimpar 501 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin)) |
95 | 94 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin)) |
96 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑦 → (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)) |
97 | 96 | cbviunv 4495 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) |
98 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) → 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) |
99 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(𝒫 ∪ 𝐽 ∩ Fin) ⊆ 𝒫 ∪ 𝐽 |
100 | 99, 91 | syl5sseqr 3617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝒫 ∪ 𝐽
∩ Fin) ⊆ 𝒫 𝑋) |
101 | | fss 5969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ (𝒫 ∪ 𝐽 ∩ Fin) ⊆ 𝒫 𝑋) → 𝑚:ℕ0⟶𝒫 𝑋) |
102 | 98, 100, 101 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) → 𝑚:ℕ0⟶𝒫 𝑋) |
103 | 102 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑚‘𝑛) ∈ 𝒫 𝑋) |
104 | 103 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑚‘𝑛) ⊆ 𝑋) |
105 | 104 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) ∧ 𝑦 ∈ (𝑚‘𝑛)) → 𝑦 ∈ 𝑋) |
106 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) ∧ 𝑦 ∈ (𝑚‘𝑛)) → 𝑛 ∈ ℕ0) |
107 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑦 → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑚)))) |
108 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (1 / (2↑𝑚)) = (1 / (2↑𝑛))) |
110 | 109 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑦(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
111 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ∈ V |
112 | 107, 110,
89, 111 | ovmpt2 6694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑛 ∈ ℕ0) → (𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
113 | 105, 106,
112 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) ∧ 𝑦 ∈ (𝑚‘𝑛)) → (𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
114 | 113 | iuneq2dv 4478 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
115 | 97, 114 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) |
116 | 115 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) |
117 | 116 | biimprd 237 |
. . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))) |
118 | 117 | ralimdva 2945 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) → (∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))) |
119 | 118 | impr 647 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)) |
120 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑚‘𝑛) = (𝑚‘𝑘)) |
121 | 120 | iuneq1d 4481 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ∪
𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)) |
122 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 = 𝑘 ∧ 𝑡 ∈ (𝑚‘𝑘)) → 𝑛 = 𝑘) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 = 𝑘 ∧ 𝑡 ∈ (𝑚‘𝑘)) → (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) |
124 | 123 | iuneq2dv 4478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ∪
𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) |
125 | 121, 124 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → ∪
𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) |
126 | 125 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))) |
127 | 126 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ℕ0 𝑋 =
∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ ∀𝑘 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) |
128 | 119, 127 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑘 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) |
129 | 1, 87, 88, 89, 90, 95, 128 | heiborlem10 32789 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) ∧ (𝑟 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑟)) → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣) |
130 | 129 | exp32 629 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟 ⊆ 𝐽 → (∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) |
131 | 86, 130 | syl5 33 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟 ∈ 𝒫 𝐽 → (∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) |
132 | 131 | ralrimiv 2948 |
. . . . . . . 8
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣)) |
133 | 132 | ex 449 |
. . . . . . 7
⊢ (𝐷 ∈ (CMet‘𝑋) → ((𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) |
134 | 133 | exlimdv 1848 |
. . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → (∃𝑚(𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) |
135 | 85, 134 | syld 46 |
. . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) |
136 | 135 | imp 444 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣)) |
137 | | eqid 2610 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
138 | 137 | iscmp 21001 |
. . . 4
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑟
→ ∃𝑣 ∈
(𝒫 𝑟 ∩
Fin)∪ 𝐽 = ∪ 𝑣))) |
139 | 8, 136, 138 | sylanbrc 695 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Comp) |
140 | 4, 139 | jca 553 |
. 2
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → (𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp)) |
141 | 2, 140 | impbii 198 |
1
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) |