Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  met2ndci Structured version   Visualization version   GIF version

Theorem met2ndci 22528
 Description: A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
Hypothesis
Ref Expression
methaus.1 𝐽 = (MetOpen‘𝐷)
Assertion
Ref Expression
met2ndci ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2nd𝜔)

Proof of Theorem met2ndci
Dummy variables 𝑛 𝑟 𝑡 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 methaus.1 . . . . 5 𝐽 = (MetOpen‘𝐷)
21mopntop 22446 . . . 4 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
32adantr 472 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ Top)
4 simpll 807 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
5 simplr1 1261 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴𝑋)
6 simprr 813 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝐴)
75, 6sseldd 3745 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝑋)
8 simprl 811 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℕ)
98nnrpd 12063 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℝ+)
109rpreccld 12075 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ+)
1110rpxrd 12066 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ*)
121blopn 22506 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (1 / 𝑥) ∈ ℝ*) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
134, 7, 11, 12syl3anc 1477 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
1413ralrimivva 3109 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
15 eqid 2760 . . . . . 6 (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))
1615fmpt2 7405 . . . . 5 (∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽 ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
1714, 16sylib 208 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
18 frn 6214 . . . 4 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽 → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽)
1917, 18syl 17 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽)
20 simpll 807 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝐷 ∈ (∞Met‘𝑋))
21 simprl 811 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝑢𝐽)
22 simprr 813 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝑧𝑢)
231mopni2 22499 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢𝐽𝑧𝑢) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
2420, 21, 22, 23syl3anc 1477 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
25 simprl 811 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
2625rphalfcld 12077 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → (𝑟 / 2) ∈ ℝ+)
27 elrp 12027 . . . . . . . 8 ((𝑟 / 2) ∈ ℝ+ ↔ ((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)))
28 nnrecl 11482 . . . . . . . 8 (((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
2927, 28sylbi 207 . . . . . . 7 ((𝑟 / 2) ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
3026, 29syl 17 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
313ad2antrr 764 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐽 ∈ Top)
32 simpr1 1234 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴𝑋)
3332ad2antrr 764 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴𝑋)
341mopnuni 22447 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
3534ad3antrrr 768 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑋 = 𝐽)
3633, 35sseqtrd 3782 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 𝐽)
37 simplrr 820 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑢)
38 simplrl 819 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑢𝐽)
39 elunii 4593 . . . . . . . . . . . . 13 ((𝑧𝑢𝑢𝐽) → 𝑧 𝐽)
4037, 38, 39syl2anc 696 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 𝐽)
4140, 35eleqtrrd 2842 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑋)
42 simpr3 1238 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ((cls‘𝐽)‘𝐴) = 𝑋)
4342ad2antrr 764 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((cls‘𝐽)‘𝐴) = 𝑋)
4441, 43eleqtrrd 2842 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
4520adantr 472 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐷 ∈ (∞Met‘𝑋))
46 simprrl 823 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℕ)
4746nnrpd 12063 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℝ+)
4847rpreccld 12075 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ+)
4948rpxrd 12066 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ*)
501blopn 22506 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ*) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
5145, 41, 49, 50syl3anc 1477 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
52 blcntr 22419 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ+) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
5345, 41, 48, 52syl3anc 1477 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
54 eqid 2760 . . . . . . . . . . 11 𝐽 = 𝐽
5554clsndisj 21081 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐴 𝐽𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
5631, 36, 44, 51, 53, 55syl32anc 1485 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
57 n0 4074 . . . . . . . . 9 (((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
5856, 57sylib 208 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
5946adantr 472 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑛 ∈ ℕ)
60 inss2 3977 . . . . . . . . . . . 12 ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ⊆ 𝐴
61 simpr 479 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
6260, 61sseldi 3742 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝐴)
63 eqidd 2761 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
64 oveq2 6821 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (1 / 𝑥) = (1 / 𝑛))
6564oveq2d 6829 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝑦(ball‘𝐷)(1 / 𝑥)) = (𝑦(ball‘𝐷)(1 / 𝑛)))
6665eqeq2d 2770 . . . . . . . . . . . 12 (𝑥 = 𝑛 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛))))
67 oveq1 6820 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (𝑦(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
6867eqeq2d 2770 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))))
6966, 68rspc2ev 3463 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑡𝐴 ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))) → ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
7059, 62, 63, 69syl3anc 1477 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
71 ovex 6841 . . . . . . . . . . 11 (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ V
72 eqeq1 2764 . . . . . . . . . . . 12 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
73722rexbidv 3195 . . . . . . . . . . 11 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
7415rnmpt2 6935 . . . . . . . . . . 11 ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = {𝑧 ∣ ∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥))}
7571, 73, 74elab2 3494 . . . . . . . . . 10 ((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
7670, 75sylibr 224 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
77 inss1 3976 . . . . . . . . . . 11 ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ⊆ (𝑧(ball‘𝐷)(1 / 𝑛))
7877, 61sseldi 3742 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
7945adantr 472 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
8049adantr 472 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ∈ ℝ*)
8141adantr 472 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧𝑋)
8233adantr 472 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐴𝑋)
8382, 62sseldd 3745 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝑋)
84 blcom 22400 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ (1 / 𝑛) ∈ ℝ*) ∧ (𝑧𝑋𝑡𝑋)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
8579, 80, 81, 83, 84syl22anc 1478 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
8678, 85mpbid 222 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)))
87 simprll 821 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑟 ∈ ℝ+)
8887adantr 472 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ+)
8988rphalfcld 12077 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ+)
9089rpxrd 12066 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ*)
91 simprrr 824 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) < (𝑟 / 2))
9287rphalfcld 12077 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ+)
93 rpre 12032 . . . . . . . . . . . . . . 15 ((1 / 𝑛) ∈ ℝ+ → (1 / 𝑛) ∈ ℝ)
94 rpre 12032 . . . . . . . . . . . . . . 15 ((𝑟 / 2) ∈ ℝ+ → (𝑟 / 2) ∈ ℝ)
95 ltle 10318 . . . . . . . . . . . . . . 15 (((1 / 𝑛) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9693, 94, 95syl2an 495 . . . . . . . . . . . . . 14 (((1 / 𝑛) ∈ ℝ+ ∧ (𝑟 / 2) ∈ ℝ+) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9748, 92, 96syl2anc 696 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9891, 97mpd 15 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ≤ (𝑟 / 2))
9998adantr 472 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ≤ (𝑟 / 2))
100 ssbl 22429 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋) ∧ ((1 / 𝑛) ∈ ℝ* ∧ (𝑟 / 2) ∈ ℝ*) ∧ (1 / 𝑛) ≤ (𝑟 / 2)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
10179, 83, 80, 90, 99, 100syl221anc 1488 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
10288rpred 12065 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ)
103101, 86sseldd 3745 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))
104 blhalf 22411 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋) ∧ (𝑟 ∈ ℝ ∧ 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
10579, 83, 102, 103, 104syl22anc 1478 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
106 simprlr 822 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
107106adantr 472 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
108105, 107sstrd 3754 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ 𝑢)
109101, 108sstrd 3754 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)
110 eleq2 2828 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧𝑤𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
111 sseq1 3767 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑤𝑢 ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢))
112110, 111anbi12d 749 . . . . . . . . . 10 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → ((𝑧𝑤𝑤𝑢) ↔ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)))
113112rspcev 3449 . . . . . . . . 9 (((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∧ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11476, 86, 109, 113syl12anc 1475 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11558, 114exlimddv 2012 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
116115anassrs 683 . . . . . 6 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11730, 116rexlimddv 3173 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11824, 117rexlimddv 3173 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
119118ralrimivva 3109 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
120 basgen2 20995 . . 3 ((𝐽 ∈ Top ∧ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽 ∧ ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
1213, 19, 119, 120syl3anc 1477 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
122121, 3eqeltrd 2839 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
123 tgclb 20976 . . . 4 (ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
124122, 123sylibr 224 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases)
125 omelon 8716 . . . . . 6 ω ∈ On
126 simpr2 1236 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ≼ ω)
127 nnex 11218 . . . . . . . . 9 ℕ ∈ V
128127xpdom2 8220 . . . . . . . 8 (𝐴 ≼ ω → (ℕ × 𝐴) ≼ (ℕ × ω))
129126, 128syl 17 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ (ℕ × ω))
130 nnenom 12973 . . . . . . . . 9 ℕ ≈ ω
131 omex 8713 . . . . . . . . . 10 ω ∈ V
132131enref 8154 . . . . . . . . 9 ω ≈ ω
133 xpen 8288 . . . . . . . . 9 ((ℕ ≈ ω ∧ ω ≈ ω) → (ℕ × ω) ≈ (ω × ω))
134130, 132, 133mp2an 710 . . . . . . . 8 (ℕ × ω) ≈ (ω × ω)
135 xpomen 9028 . . . . . . . 8 (ω × ω) ≈ ω
136134, 135entri 8175 . . . . . . 7 (ℕ × ω) ≈ ω
137 domentr 8180 . . . . . . 7 (((ℕ × 𝐴) ≼ (ℕ × ω) ∧ (ℕ × ω) ≈ ω) → (ℕ × 𝐴) ≼ ω)
138129, 136, 137sylancl 697 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ ω)
139 ondomen 9050 . . . . . 6 ((ω ∈ On ∧ (ℕ × 𝐴) ≼ ω) → (ℕ × 𝐴) ∈ dom card)
140125, 138, 139sylancr 698 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ∈ dom card)
141 ffn 6206 . . . . . . 7 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽 → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
14217, 141syl 17 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
143 dffn4 6282 . . . . . 6 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴) ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
144142, 143sylib 208 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
145 fodomnum 9070 . . . . 5 ((ℕ × 𝐴) ∈ dom card → ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴)))
146140, 144, 145sylc 65 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴))
147 domtr 8174 . . . 4 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴) ∧ (ℕ × 𝐴) ≼ ω) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
148146, 138, 147syl2anc 696 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
149 2ndci 21453 . . 3 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ∧ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2nd𝜔)
150124, 148, 149syl2anc 696 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2nd𝜔)
151121, 150eqeltrrd 2840 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2nd𝜔)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632  ∃wex 1853   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058  ∪ cuni 4588   class class class wbr 4804   × cxp 5264  dom cdm 5266  ran crn 5267  Oncon0 5884   Fn wfn 6044  ⟶wf 6045  –onto→wfo 6047  ‘cfv 6049  (class class class)co 6813   ↦ cmpt2 6815  ωcom 7230   ≈ cen 8118   ≼ cdom 8119  cardccrd 8951  ℝcr 10127  0cc0 10128  1c1 10129  ℝ*cxr 10265   < clt 10266   ≤ cle 10267   / cdiv 10876  ℕcn 11212  2c2 11262  ℝ+crp 12025  topGenctg 16300  ∞Metcxmt 19933  ballcbl 19935  MetOpencmopn 19938  Topctop 20900  TopBasesctb 20951  clsccl 21024  2nd𝜔c2ndc 21443 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-acn 8958  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-n0 11485  df-z 11570  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-topgen 16306  df-psmet 19940  df-xmet 19941  df-bl 19943  df-mopn 19944  df-top 20901  df-topon 20918  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-2ndc 21445 This theorem is referenced by:  met2ndc  22529
 Copyright terms: Public domain W3C validator