This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem met2ndci

Description: A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis methaus.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion met2ndci ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐽 ∈ 2ndω )

Proof

Step Hyp Ref Expression
1 methaus.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐽 ∈ Top )
4 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5 simplr1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝐴 ⊆ 𝑋 )
6 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
7 5 6 sseldd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝑋 )
8 simprl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℕ )
9 8 nnrpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℝ+ )
10 9 rpreccld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 1 / 𝑥 ) ∈ ℝ+ )
11 10 rpxrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 1 / 𝑥 ) ∈ ℝ* )
12 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( 1 / 𝑥 ) ∈ ℝ* ) → ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ∈ 𝐽 )
13 4 7 11 12 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ∈ 𝐽 )
14 13 ralrimivva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ∈ 𝐽 )
15 eqid ⊢ ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) = ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) )
16 15 fmpo ⊢ ( ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ∈ 𝐽 ↔ ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) : ( ℕ × 𝐴 ) ⟶ 𝐽 )
17 14 16 sylib ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) : ( ℕ × 𝐴 ) ⟶ 𝐽 )
18 17 frnd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ⊆ 𝐽 )
19 simpll ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20 simprl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) → 𝑢 ∈ 𝐽 )
21 simprr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) → 𝑧 ∈ 𝑢 )
22 1 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 )
23 19 20 21 22 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 )
24 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ+ )
25 24 rphalfcld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
26 elrp ⊢ ( ( 𝑟 / 2 ) ∈ ℝ+ ↔ ( ( 𝑟 / 2 ) ∈ ℝ ∧ 0 < ( 𝑟 / 2 ) ) )
27 nnrecl ⊢ ( ( ( 𝑟 / 2 ) ∈ ℝ ∧ 0 < ( 𝑟 / 2 ) ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) )
28 26 27 sylbi ⊢ ( ( 𝑟 / 2 ) ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) )
29 25 28 syl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) )
30 3 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝐽 ∈ Top )
31 simpr1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐴 ⊆ 𝑋 )
32 31 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝐴 ⊆ 𝑋 )
33 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
34 33 ad3antrrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑋 = ∪ 𝐽 )
35 32 34 sseqtrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝐴 ⊆ ∪ 𝐽 )
36 simplrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑧 ∈ 𝑢 )
37 simplrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑢 ∈ 𝐽 )
38 elunii ⊢ ( ( 𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝐽 ) → 𝑧 ∈ ∪ 𝐽 )
39 36 37 38 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑧 ∈ ∪ 𝐽 )
40 39 34 eleqtrrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑧 ∈ 𝑋 )
41 simpr3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
42 41 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 )
43 40 42 eleqtrrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
44 19 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
45 simprrl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑛 ∈ ℕ )
46 45 nnrpd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑛 ∈ ℝ+ )
47 46 rpreccld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ+ )
48 47 rpxrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ* )
49 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ ( 1 / 𝑛 ) ∈ ℝ* ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 )
50 44 40 48 49 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 )
51 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ ( 1 / 𝑛 ) ∈ ℝ+ ) → 𝑧 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
52 44 40 47 51 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑧 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
53 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
54 53 clsndisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 ∧ 𝑧 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) ) → ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ≠ ∅ )
55 30 35 43 50 52 54 syl32anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ≠ ∅ )
56 n0 ⊢ ( ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ≠ ∅ ↔ ∃ 𝑡 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) )
57 55 56 sylib ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ∃ 𝑡 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) )
58 45 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑛 ∈ ℕ )
59 simpr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) )
60 59 elin2d ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑡 ∈ 𝐴 )
61 eqidd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
62 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 1 / 𝑥 ) = ( 1 / 𝑛 ) )
63 62 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
64 63 eqeq2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ↔ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) )
65 oveq1 ⊢ ( 𝑦 = 𝑡 → ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
66 65 eqeq2d ⊢ ( 𝑦 = 𝑡 → ( ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ↔ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) )
67 64 66 rspc2ev ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ 𝐴 ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) )
68 58 60 61 67 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ 𝐴 ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) )
69 ovex ⊢ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ V
70 eqeq1 ⊢ ( 𝑧 = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) → ( 𝑧 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ↔ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) )
71 70 2rexbidv ⊢ ( 𝑧 = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) → ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ 𝐴 ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) )
72 15 rnmpo ⊢ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) }
73 69 71 72 elab2 ⊢ ( ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ 𝐴 ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) )
74 68 73 sylibr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) )
75 59 elin1d ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑡 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
76 44 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
77 48 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 1 / 𝑛 ) ∈ ℝ* )
78 40 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑧 ∈ 𝑋 )
79 32 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝐴 ⊆ 𝑋 )
80 79 60 sseldd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑡 ∈ 𝑋 )
81 blcom ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1 / 𝑛 ) ∈ ℝ* ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋 ) ) → ( 𝑡 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ↔ 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) )
82 76 77 78 80 81 syl22anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ↔ 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) )
83 75 82 mpbid ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) )
84 simprll ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → 𝑟 ∈ ℝ+ )
85 84 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑟 ∈ ℝ+ )
86 85 rphalfcld ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
87 86 rpxrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑟 / 2 ) ∈ ℝ* )
88 simprrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 1 / 𝑛 ) < ( 𝑟 / 2 ) )
89 84 rphalfcld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
90 rpre ⊢ ( ( 1 / 𝑛 ) ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ )
91 rpre ⊢ ( ( 𝑟 / 2 ) ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ )
92 ltle ⊢ ( ( ( 1 / 𝑛 ) ∈ ℝ ∧ ( 𝑟 / 2 ) ∈ ℝ ) → ( ( 1 / 𝑛 ) < ( 𝑟 / 2 ) → ( 1 / 𝑛 ) ≤ ( 𝑟 / 2 ) ) )
93 90 91 92 syl2an ⊢ ( ( ( 1 / 𝑛 ) ∈ ℝ+ ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → ( ( 1 / 𝑛 ) < ( 𝑟 / 2 ) → ( 1 / 𝑛 ) ≤ ( 𝑟 / 2 ) ) )
94 47 89 93 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( ( 1 / 𝑛 ) < ( 𝑟 / 2 ) → ( 1 / 𝑛 ) ≤ ( 𝑟 / 2 ) ) )
95 88 94 mpd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 1 / 𝑛 ) ≤ ( 𝑟 / 2 ) )
96 95 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 1 / 𝑛 ) ≤ ( 𝑟 / 2 ) )
97 ssbl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ) ∧ ( ( 1 / 𝑛 ) ∈ ℝ* ∧ ( 𝑟 / 2 ) ∈ ℝ* ) ∧ ( 1 / 𝑛 ) ≤ ( 𝑟 / 2 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
98 76 80 77 87 96 97 syl221anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
99 85 rpred ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑟 ∈ ℝ )
100 98 83 sseldd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
101 blhalf ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ ∧ 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) )
102 76 80 99 100 101 syl22anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) )
103 simprlr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 )
104 103 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 )
105 102 104 sstrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ 𝑢 )
106 98 105 sstrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ⊆ 𝑢 )
107 eleq2 ⊢ ( 𝑤 = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ) )
108 sseq1 ⊢ ( 𝑤 = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) → ( 𝑤 ⊆ 𝑢 ↔ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ⊆ 𝑢 ) )
109 107 108 anbi12d ⊢ ( 𝑤 = ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ↔ ( 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∧ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ⊆ 𝑢 ) ) )
110 109 rspcev ⊢ ( ( ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ∧ ( 𝑧 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∧ ( 𝑡 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
111 74 83 106 110 syl12anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
112 57 111 exlimddv ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
113 112 anassrs ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) < ( 𝑟 / 2 ) ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
114 29 113 rexlimddv ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
115 23 114 rexlimddv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
116 115 ralrimivva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ∀ 𝑢 ∈ 𝐽 ∀ 𝑧 ∈ 𝑢 ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
117 basgen2 ⊢ ( ( 𝐽 ∈ Top ∧ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ⊆ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ∀ 𝑧 ∈ 𝑢 ∃ 𝑤 ∈ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( topGen ‘ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ) = 𝐽 )
118 3 18 116 117 syl3anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( topGen ‘ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ) = 𝐽 )
119 118 3 eqeltrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( topGen ‘ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ) ∈ Top )
120 tgclb ⊢ ( ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ∈ TopBases ↔ ( topGen ‘ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ) ∈ Top )
121 119 120 sylibr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ∈ TopBases )
122 omelon ⊢ ω ∈ On
123 simpr2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐴 ≼ ω )
124 nnex ⊢ ℕ ∈ V
125 124 xpdom2 ⊢ ( 𝐴 ≼ ω → ( ℕ × 𝐴 ) ≼ ( ℕ × ω ) )
126 123 125 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ℕ × 𝐴 ) ≼ ( ℕ × ω ) )
127 nnenom ⊢ ℕ ≈ ω
128 omex ⊢ ω ∈ V
129 128 enref ⊢ ω ≈ ω
130 xpen ⊢ ( ( ℕ ≈ ω ∧ ω ≈ ω ) → ( ℕ × ω ) ≈ ( ω × ω ) )
131 127 129 130 mp2an ⊢ ( ℕ × ω ) ≈ ( ω × ω )
132 xpomen ⊢ ( ω × ω ) ≈ ω
133 131 132 entri ⊢ ( ℕ × ω ) ≈ ω
134 domentr ⊢ ( ( ( ℕ × 𝐴 ) ≼ ( ℕ × ω ) ∧ ( ℕ × ω ) ≈ ω ) → ( ℕ × 𝐴 ) ≼ ω )
135 126 133 134 sylancl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ℕ × 𝐴 ) ≼ ω )
136 ondomen ⊢ ( ( ω ∈ On ∧ ( ℕ × 𝐴 ) ≼ ω ) → ( ℕ × 𝐴 ) ∈ dom card )
137 122 135 136 sylancr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( ℕ × 𝐴 ) ∈ dom card )
138 17 ffnd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) Fn ( ℕ × 𝐴 ) )
139 dffn4 ⊢ ( ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) Fn ( ℕ × 𝐴 ) ↔ ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) : ( ℕ × 𝐴 ) –onto→ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) )
140 138 139 sylib ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) : ( ℕ × 𝐴 ) –onto→ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) )
141 fodomnum ⊢ ( ( ℕ × 𝐴 ) ∈ dom card → ( ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) : ( ℕ × 𝐴 ) –onto→ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) → ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ≼ ( ℕ × 𝐴 ) ) )
142 137 140 141 sylc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ≼ ( ℕ × 𝐴 ) )
143 domtr ⊢ ( ( ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ≼ ( ℕ × 𝐴 ) ∧ ( ℕ × 𝐴 ) ≼ ω ) → ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ≼ ω )
144 142 135 143 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ≼ ω )
145 2ndci ⊢ ( ( ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ∈ TopBases ∧ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ) ∈ 2ndω )
146 121 144 145 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → ( topGen ‘ ran ( 𝑥 ∈ ℕ , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball ‘ 𝐷 ) ( 1 / 𝑥 ) ) ) ) ∈ 2ndω )
147 118 146 eqeltrrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) = 𝑋 ) ) → 𝐽 ∈ 2ndω )