| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | heibor.1 | . . 3
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 2 | 1 | heibor1 37817 | . 2
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) → (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) | 
| 3 |  | cmetmet 25320 | . . . 4
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 4 | 3 | adantr 480 | . . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐷 ∈ (Met‘𝑋)) | 
| 5 |  | metxmet 24344 | . . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 6 | 1 | mopntop 24450 | . . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) | 
| 7 | 3, 5, 6 | 3syl 18 | . . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐽 ∈ Top) | 
| 8 | 7 | adantr 480 | . . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Top) | 
| 9 |  | istotbnd 37776 | . . . . . . . . . . . . 13
⊢ (𝐷 ∈ (TotBnd‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)))) | 
| 10 | 9 | simprbi 496 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ ℝ+
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟))) | 
| 11 |  | 2nn 12339 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ | 
| 12 |  | nnexpcl 14115 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) | 
| 13 | 11, 12 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (2↑𝑛) ∈
ℕ) | 
| 14 | 13 | nnrpd 13075 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (2↑𝑛) ∈
ℝ+) | 
| 15 | 14 | rpreccld 13087 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (1 / (2↑𝑛))
∈ ℝ+) | 
| 16 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = (1 / (2↑𝑛)) → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 17 | 16 | eqeq2d 2748 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = (1 / (2↑𝑛)) → (𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 18 | 17 | rexbidv 3179 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 = (1 / (2↑𝑛)) → (∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 19 | 18 | ralbidv 3178 | . . . . . . . . . . . . . . 15
⊢ (𝑟 = (1 / (2↑𝑛)) → (∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟) ↔ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 20 | 19 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑟 = (1 / (2↑𝑛)) → ((∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ (∪ 𝑢 = 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) | 
| 21 | 20 | rexbidv 3179 | . . . . . . . . . . . . 13
⊢ (𝑟 = (1 / (2↑𝑛)) → (∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ↔ ∃𝑢 ∈ Fin (∪
𝑢 = 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) | 
| 22 | 21 | rspccva 3621 | . . . . . . . . . . . 12
⊢
((∀𝑟 ∈
ℝ+ ∃𝑢 ∈ Fin (∪
𝑢 = 𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)𝑟)) ∧ (1 / (2↑𝑛)) ∈ ℝ+) →
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 23 | 10, 15, 22 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ (TotBnd‘𝑋) ∧ 𝑛 ∈ ℕ0) →
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 24 | 23 | expcom 413 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝐷 ∈
(TotBnd‘𝑋) →
∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) | 
| 25 | 24 | adantl 481 | . . . . . . . . 9
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) | 
| 26 |  | oveq1 7438 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑚‘𝑣) → (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 27 | 26 | eqeq2d 2748 | . . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑚‘𝑣) → (𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 28 | 27 | ac6sfi 9320 | . . . . . . . . . . . . 13
⊢ ((𝑢 ∈ Fin ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 29 | 28 | adantrl 716 | . . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 30 | 29 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 31 |  | simp3l 1202 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:𝑢⟶𝑋) | 
| 32 | 31 | frnd 6744 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ⊆ 𝑋) | 
| 33 | 1 | mopnuni 24451 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 34 | 3, 5, 33 | 3syl 18 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 35 | 34 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → 𝑋 = ∪
𝐽) | 
| 36 | 35 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = ∪ 𝐽) | 
| 37 | 32, 36 | sseqtrd 4020 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ⊆ ∪ 𝐽) | 
| 38 | 1 | fvexi 6920 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 ∈ V | 
| 39 | 38 | uniex 7761 | . . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽
∈ V | 
| 40 | 39 | elpw2 5334 | . . . . . . . . . . . . . . . . 17
⊢ (ran
𝑚 ∈ 𝒫 ∪ 𝐽
↔ ran 𝑚 ⊆ ∪ 𝐽) | 
| 41 | 37, 40 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ 𝒫 ∪ 𝐽) | 
| 42 |  | simp2l 1200 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑢 ∈ Fin) | 
| 43 |  | ffn 6736 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑚:𝑢⟶𝑋 → 𝑚 Fn 𝑢) | 
| 44 |  | dffn4 6826 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 Fn 𝑢 ↔ 𝑚:𝑢–onto→ran 𝑚) | 
| 45 | 43, 44 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚:𝑢⟶𝑋 → 𝑚:𝑢–onto→ran 𝑚) | 
| 46 |  | fofi 9351 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ Fin ∧ 𝑚:𝑢–onto→ran 𝑚) → ran 𝑚 ∈ Fin) | 
| 47 | 45, 46 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ Fin ∧ 𝑚:𝑢⟶𝑋) → ran 𝑚 ∈ Fin) | 
| 48 | 42, 31, 47 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ Fin) | 
| 49 | 41, 48 | elind 4200 | . . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ran 𝑚 ∈ (𝒫 ∪ 𝐽
∩ Fin)) | 
| 50 | 26 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑚‘𝑣) → (𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 ∈ ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 51 | 50 | rexrn 7107 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 Fn 𝑢 → (∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣 ∈ 𝑢 𝑟 ∈ ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 52 |  | eliun 4995 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑦 ∈ ran 𝑚 𝑟 ∈ (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 53 |  | eliun 4995 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))) ↔ ∃𝑣 ∈ 𝑢 𝑟 ∈ ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 54 | 51, 52, 53 | 3bitr4g 314 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 Fn 𝑢 → (𝑟 ∈ ∪
𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑟 ∈ ∪
𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 55 | 54 | eqrdv 2735 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 Fn 𝑢 → ∪
𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 56 | 31, 43, 55 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 57 |  | simp3r 1203 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 58 |  | uniiun 5058 | . . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑢 =
∪ 𝑣 ∈ 𝑢 𝑣 | 
| 59 |  | iuneq2 5011 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑣 ∈
𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → ∪ 𝑣 ∈ 𝑢 𝑣 = ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 60 | 58, 59 | eqtrid 2789 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑣 ∈
𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))) → ∪ 𝑢 = ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 61 | 57, 60 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∪
𝑢 = ∪ 𝑣 ∈ 𝑢 ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 62 |  | simp2r 1201 | . . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∪
𝑢 = 𝑋) | 
| 63 | 56, 61, 62 | 3eqtr2rd 2784 | . . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑋 = ∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 64 |  | iuneq1 5008 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = ran 𝑚 → ∪
𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 65 | 64 | rspceeqv 3645 | . . . . . . . . . . . . . . 15
⊢ ((ran
𝑚 ∈ (𝒫 ∪ 𝐽
∩ Fin) ∧ 𝑋 =
∪ 𝑦 ∈ ran 𝑚(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 66 | 49, 63, 65 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋) ∧ (𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛))))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 67 | 66 | 3expia 1122 | . . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ ∪ 𝑢 =
𝑋)) → ((𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 68 | 67 | adantrrr 725 | . . . . . . . . . . . 12
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ((𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 69 | 68 | exlimdv 1933 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → (∃𝑚(𝑚:𝑢⟶𝑋 ∧ ∀𝑣 ∈ 𝑢 𝑣 = ((𝑚‘𝑣)(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 70 | 30, 69 | mpd 15 | . . . . . . . . . 10
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) ∧ (𝑢 ∈ Fin ∧ (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 71 | 70 | rexlimdvaa 3156 | . . . . . . . . 9
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) →
(∃𝑢 ∈ Fin (∪ 𝑢 =
𝑋 ∧ ∀𝑣 ∈ 𝑢 ∃𝑦 ∈ 𝑋 𝑣 = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 72 | 25, 71 | syld 47 | . . . . . . . 8
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑛 ∈ ℕ0) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 73 | 72 | ralrimdva 3154 | . . . . . . 7
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑛 ∈ ℕ0 ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 74 | 39 | pwex 5380 | . . . . . . . . 9
⊢ 𝒫
∪ 𝐽 ∈ V | 
| 75 | 74 | inex1 5317 | . . . . . . . 8
⊢
(𝒫 ∪ 𝐽 ∩ Fin) ∈ V | 
| 76 |  | nn0ennn 14020 | . . . . . . . . 9
⊢
ℕ0 ≈ ℕ | 
| 77 |  | nnenom 14021 | . . . . . . . . 9
⊢ ℕ
≈ ω | 
| 78 | 76, 77 | entri 9048 | . . . . . . . 8
⊢
ℕ0 ≈ ω | 
| 79 |  | iuneq1 5008 | . . . . . . . . 9
⊢ (𝑡 = (𝑚‘𝑛) → ∪
𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) = ∪
𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 80 | 79 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑡 = (𝑚‘𝑛) → (𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ↔ 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 81 | 75, 78, 80 | axcc4 10479 | . . . . . . 7
⊢
(∀𝑛 ∈
ℕ0 ∃𝑡 ∈ (𝒫 ∪ 𝐽
∩ Fin)𝑋 = ∪ 𝑦 ∈ 𝑡 (𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∃𝑚(𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 82 | 73, 81 | syl6 35 | . . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∃𝑚(𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))))) | 
| 83 |  | elpwi 4607 | . . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 𝐽 → 𝑟 ⊆ 𝐽) | 
| 84 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣} = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣} | 
| 85 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
{〈𝑡, 𝑘〉 ∣ (𝑘 ∈ ℕ0
∧ 𝑡 ∈ (𝑚‘𝑘) ∧ (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣})} = {〈𝑡, 𝑘〉 ∣ (𝑘 ∈ ℕ0 ∧ 𝑡 ∈ (𝑚‘𝑘) ∧ (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘) ∈ {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)𝑢 ⊆ ∪ 𝑣})} | 
| 86 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚)))) | 
| 87 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝐷 ∈ (CMet‘𝑋)) | 
| 88 | 34 | pweqd 4617 | . . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝒫 𝑋 = 𝒫 ∪ 𝐽) | 
| 89 | 88 | ineq1d 4219 | . . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝒫 𝑋 ∩ Fin) = (𝒫 ∪ 𝐽
∩ Fin)) | 
| 90 | 89 | feq3d 6723 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin) ↔ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin))) | 
| 91 | 90 | biimpar 477 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin)) | 
| 92 | 91 | adantrr 717 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → 𝑚:ℕ0⟶(𝒫 𝑋 ∩ Fin)) | 
| 93 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑦 → (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)) | 
| 94 | 93 | cbviunv 5040 | . . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) | 
| 95 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) → 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) | 
| 96 |  | inss1 4237 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(𝒫 ∪ 𝐽 ∩ Fin) ⊆ 𝒫 ∪ 𝐽 | 
| 97 | 96, 88 | sseqtrrid 4027 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝒫 ∪ 𝐽
∩ Fin) ⊆ 𝒫 𝑋) | 
| 98 |  | fss 6752 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ (𝒫 ∪ 𝐽 ∩ Fin) ⊆ 𝒫 𝑋) → 𝑚:ℕ0⟶𝒫 𝑋) | 
| 99 | 95, 97, 98 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) → 𝑚:ℕ0⟶𝒫 𝑋) | 
| 100 | 99 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑚‘𝑛) ∈ 𝒫 𝑋) | 
| 101 | 100 | elpwid 4609 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑚‘𝑛) ⊆ 𝑋) | 
| 102 | 101 | sselda 3983 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) ∧ 𝑦 ∈ (𝑚‘𝑛)) → 𝑦 ∈ 𝑋) | 
| 103 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) ∧ 𝑦 ∈ (𝑚‘𝑛)) → 𝑛 ∈ ℕ0) | 
| 104 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑦 → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑚)))) | 
| 105 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛)) | 
| 106 | 105 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (1 / (2↑𝑚)) = (1 / (2↑𝑛))) | 
| 107 | 106 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑦(ball‘𝐷)(1 / (2↑𝑚))) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 108 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(ball‘𝐷)(1 / (2↑𝑛))) ∈ V | 
| 109 | 104, 107,
86, 108 | ovmpo 7593 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ 𝑋 ∧ 𝑛 ∈ ℕ0) → (𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 110 | 102, 103,
109 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) ∧ 𝑦 ∈ (𝑚‘𝑛)) → (𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 111 | 110 | iuneq2dv 5016 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 112 | 94, 111 | eqtrid 2789 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) | 
| 113 | 112 | eqeq2d 2748 | . . . . . . . . . . . . . . . 16
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) | 
| 114 | 113 | biimprd 248 | . . . . . . . . . . . . . . 15
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) ∧ 𝑛 ∈
ℕ0) → (𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))) | 
| 115 | 114 | ralimdva 3167 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin)) → (∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))) → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛))) | 
| 116 | 115 | impr 454 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)) | 
| 117 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑚‘𝑛) = (𝑚‘𝑘)) | 
| 118 | 117 | iuneq1d 5019 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ∪
𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛)) | 
| 119 |  | simpl 482 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 = 𝑘 ∧ 𝑡 ∈ (𝑚‘𝑘)) → 𝑛 = 𝑘) | 
| 120 | 119 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 = 𝑘 ∧ 𝑡 ∈ (𝑚‘𝑘)) → (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = (𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) | 
| 121 | 120 | iuneq2dv 5016 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ∪
𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) | 
| 122 | 118, 121 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → ∪
𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) | 
| 123 | 122 | eqeq2d 2748 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → (𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘))) | 
| 124 | 123 | cbvralvw 3237 | . . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ℕ0 𝑋 =
∪ 𝑡 ∈ (𝑚‘𝑛)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑛) ↔ ∀𝑘 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) | 
| 125 | 116, 124 | sylib 218 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑘 ∈ ℕ0 𝑋 = ∪ 𝑡 ∈ (𝑚‘𝑘)(𝑡(𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))𝑘)) | 
| 126 | 1, 84, 85, 86, 87, 92, 125 | heiborlem10 37827 | . . . . . . . . . . 11
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) ∧ (𝑟 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑟)) → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣) | 
| 127 | 126 | exp32 420 | . . . . . . . . . 10
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟 ⊆ 𝐽 → (∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) | 
| 128 | 83, 127 | syl5 34 | . . . . . . . . 9
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → (𝑟 ∈ 𝒫 𝐽 → (∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) | 
| 129 | 128 | ralrimiv 3145 | . . . . . . . 8
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛))))) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣)) | 
| 130 | 129 | ex 412 | . . . . . . 7
⊢ (𝐷 ∈ (CMet‘𝑋) → ((𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) | 
| 131 | 130 | exlimdv 1933 | . . . . . 6
⊢ (𝐷 ∈ (CMet‘𝑋) → (∃𝑚(𝑚:ℕ0⟶(𝒫 ∪ 𝐽
∩ Fin) ∧ ∀𝑛
∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝑚‘𝑛)(𝑦(ball‘𝐷)(1 / (2↑𝑛)))) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) | 
| 132 | 82, 131 | syld 47 | . . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → (𝐷 ∈ (TotBnd‘𝑋) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣))) | 
| 133 | 132 | imp 406 | . . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪
𝑟 → ∃𝑣 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 =
∪ 𝑣)) | 
| 134 |  | eqid 2737 | . . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 135 | 134 | iscmp 23396 | . . . 4
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪
𝐽 = ∪ 𝑟
→ ∃𝑣 ∈
(𝒫 𝑟 ∩
Fin)∪ 𝐽 = ∪ 𝑣))) | 
| 136 | 8, 133, 135 | sylanbrc 583 | . . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → 𝐽 ∈ Comp) | 
| 137 | 4, 136 | jca 511 | . 2
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋)) → (𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp)) | 
| 138 | 2, 137 | impbii 209 | 1
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐽 ∈ Comp) ↔ (𝐷 ∈ (CMet‘𝑋) ∧ 𝐷 ∈ (TotBnd‘𝑋))) |