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

Theorem met2ndci 22524
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 22442 . . . 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 3741 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝑋)
8 simprl 811 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℕ)
98nnrpd 12059 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℝ+)
109rpreccld 12071 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ+)
1110rpxrd 12062 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ*)
121blopn 22502 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (1 / 𝑥) ∈ ℝ*) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
134, 7, 11, 12syl3anc 1477 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
1413ralrimivva 3105 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
15 eqid 2756 . . . . . 6 (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))
1615fmpt2 7401 . . . . 5 (∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽 ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
1714, 16sylib 208 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
18 frn 6210 . . . 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 22495 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢𝐽𝑧𝑢) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
2420, 21, 22, 23syl3anc 1477 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
25 simprl 811 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
2625rphalfcld 12073 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → (𝑟 / 2) ∈ ℝ+)
27 elrp 12023 . . . . . . . 8 ((𝑟 / 2) ∈ ℝ+ ↔ ((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)))
28 nnrecl 11478 . . . . . . . 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 22443 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
3534ad3antrrr 768 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑋 = 𝐽)
3633, 35sseqtrd 3778 . . . . . . . . . 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 4589 . . . . . . . . . . . . 13 ((𝑧𝑢𝑢𝐽) → 𝑧 𝐽)
4037, 38, 39syl2anc 696 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 𝐽)
4140, 35eleqtrrd 2838 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑋)
42 simpr3 1238 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ((cls‘𝐽)‘𝐴) = 𝑋)
4342ad2antrr 764 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((cls‘𝐽)‘𝐴) = 𝑋)
4441, 43eleqtrrd 2838 . . . . . . . . . 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 12059 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℝ+)
4847rpreccld 12071 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ+)
4948rpxrd 12062 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ*)
501blopn 22502 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ*) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
5145, 41, 49, 50syl3anc 1477 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
52 blcntr 22415 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ+) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
5345, 41, 48, 52syl3anc 1477 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
54 eqid 2756 . . . . . . . . . . 11 𝐽 = 𝐽
5554clsndisj 21077 . . . . . . . . . 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 4070 . . . . . . . . 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 3973 . . . . . . . . . . . 12 ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ⊆ 𝐴
61 simpr 479 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
6260, 61sseldi 3738 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝐴)
63 eqidd 2757 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
64 oveq2 6817 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (1 / 𝑥) = (1 / 𝑛))
6564oveq2d 6825 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝑦(ball‘𝐷)(1 / 𝑥)) = (𝑦(ball‘𝐷)(1 / 𝑛)))
6665eqeq2d 2766 . . . . . . . . . . . 12 (𝑥 = 𝑛 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛))))
67 oveq1 6816 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (𝑦(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
6867eqeq2d 2766 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))))
6966, 68rspc2ev 3459 . . . . . . . . . . 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 6837 . . . . . . . . . . 11 (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ V
72 eqeq1 2760 . . . . . . . . . . . 12 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
73722rexbidv 3191 . . . . . . . . . . 11 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
7415rnmpt2 6931 . . . . . . . . . . 11 ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = {𝑧 ∣ ∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥))}
7571, 73, 74elab2 3490 . . . . . . . . . 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 3972 . . . . . . . . . . 11 ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ⊆ (𝑧(ball‘𝐷)(1 / 𝑛))
7877, 61sseldi 3738 . . . . . . . . . 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 3741 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝑋)
84 blcom 22396 . . . . . . . . . . 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 12073 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ+)
9089rpxrd 12062 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ*)
91 simprrr 824 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) < (𝑟 / 2))
9287rphalfcld 12073 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ+)
93 rpre 12028 . . . . . . . . . . . . . . 15 ((1 / 𝑛) ∈ ℝ+ → (1 / 𝑛) ∈ ℝ)
94 rpre 12028 . . . . . . . . . . . . . . 15 ((𝑟 / 2) ∈ ℝ+ → (𝑟 / 2) ∈ ℝ)
95 ltle 10314 . . . . . . . . . . . . . . 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 22425 . . . . . . . . . . 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 12061 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ)
103101, 86sseldd 3741 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))
104 blhalf 22407 . . . . . . . . . . . 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 3750 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ 𝑢)
109101, 108sstrd 3750 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)
110 eleq2 2824 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧𝑤𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
111 sseq1 3763 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑤𝑢 ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢))
112110, 111anbi12d 749 . . . . . . . . . 10 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → ((𝑧𝑤𝑤𝑢) ↔ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)))
113112rspcev 3445 . . . . . . . . 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 2008 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
116115anassrs 683 . . . . . 6 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11730, 116rexlimddv 3169 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11824, 117rexlimddv 3169 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
119118ralrimivva 3105 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
120 basgen2 20991 . . 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 2835 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
123 tgclb 20972 . . . 4 (ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
124122, 123sylibr 224 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases)
125 omelon 8712 . . . . . 6 ω ∈ On
126 simpr2 1236 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ≼ ω)
127 nnex 11214 . . . . . . . . 9 ℕ ∈ V
128127xpdom2 8216 . . . . . . . 8 (𝐴 ≼ ω → (ℕ × 𝐴) ≼ (ℕ × ω))
129126, 128syl 17 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ (ℕ × ω))
130 nnenom 12969 . . . . . . . . 9 ℕ ≈ ω
131 omex 8709 . . . . . . . . . 10 ω ∈ V
132131enref 8150 . . . . . . . . 9 ω ≈ ω
133 xpen 8284 . . . . . . . . 9 ((ℕ ≈ ω ∧ ω ≈ ω) → (ℕ × ω) ≈ (ω × ω))
134130, 132, 133mp2an 710 . . . . . . . 8 (ℕ × ω) ≈ (ω × ω)
135 xpomen 9024 . . . . . . . 8 (ω × ω) ≈ ω
136134, 135entri 8171 . . . . . . 7 (ℕ × ω) ≈ ω
137 domentr 8176 . . . . . . 7 (((ℕ × 𝐴) ≼ (ℕ × ω) ∧ (ℕ × ω) ≈ ω) → (ℕ × 𝐴) ≼ ω)
138129, 136, 137sylancl 697 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ ω)
139 ondomen 9046 . . . . . 6 ((ω ∈ On ∧ (ℕ × 𝐴) ≼ ω) → (ℕ × 𝐴) ∈ dom card)
140125, 138, 139sylancr 698 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ∈ dom card)
141 ffn 6202 . . . . . . 7 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽 → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
14217, 141syl 17 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
143 dffn4 6278 . . . . . 6 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴) ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
144142, 143sylib 208 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
145 fodomnum 9066 . . . . 5 ((ℕ × 𝐴) ∈ dom card → ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴)))
146140, 144, 145sylc 65 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴))
147 domtr 8170 . . . 4 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴) ∧ (ℕ × 𝐴) ≼ ω) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
148146, 138, 147syl2anc 696 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
149 2ndci 21449 . . 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 2836 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2nd𝜔)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1628  wex 1849  wcel 2135  wne 2928  wral 3046  wrex 3047  cin 3710  wss 3711  c0 4054   cuni 4584   class class class wbr 4800   × cxp 5260  dom cdm 5262  ran crn 5263  Oncon0 5880   Fn wfn 6040  wf 6041  ontowfo 6043  cfv 6045  (class class class)co 6809  cmpt2 6811  ωcom 7226  cen 8114  cdom 8115  cardccrd 8947  cr 10123  0cc0 10124  1c1 10125  *cxr 10261   < clt 10262  cle 10263   / cdiv 10872  cn 11208  2c2 11258  +crp 12021  topGenctg 16296  ∞Metcxmt 19929  ballcbl 19931  MetOpencmopn 19934  Topctop 20896  TopBasesctb 20947  clsccl 21020  2nd𝜔c2ndc 21439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-inf2 8707  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201  ax-pre-sup 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-iin 4671  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-map 8021  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-sup 8509  df-inf 8510  df-oi 8576  df-card 8951  df-acn 8954  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-2 11267  df-n0 11481  df-z 11566  df-uz 11876  df-q 11978  df-rp 12022  df-xneg 12135  df-xadd 12136  df-xmul 12137  df-topgen 16302  df-psmet 19936  df-xmet 19937  df-bl 19939  df-mopn 19940  df-top 20897  df-topon 20914  df-bases 20948  df-cld 21021  df-ntr 21022  df-cls 21023  df-2ndc 21441
This theorem is referenced by:  met2ndc  22525
  Copyright terms: Public domain W3C validator