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

Theorem met2ndci 22540
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 22458 . . . 4 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
32adantr 468 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ Top)
4 simpll 774 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
5 simplr1 1268 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴𝑋)
6 simprr 780 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝐴)
75, 6sseldd 3799 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝑋)
8 simprl 778 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℕ)
98nnrpd 12084 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℝ+)
109rpreccld 12096 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ+)
1110rpxrd 12087 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ*)
121blopn 22518 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (1 / 𝑥) ∈ ℝ*) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
134, 7, 11, 12syl3anc 1483 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
1413ralrimivva 3159 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
15 eqid 2806 . . . . . 6 (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))
1615fmpt2 7470 . . . . 5 (∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽 ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
1714, 16sylib 209 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
1817frnd 6263 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽)
19 simpll 774 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝐷 ∈ (∞Met‘𝑋))
20 simprl 778 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝑢𝐽)
21 simprr 780 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝑧𝑢)
221mopni2 22511 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢𝐽𝑧𝑢) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
2319, 20, 21, 22syl3anc 1483 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
24 simprl 778 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
2524rphalfcld 12098 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → (𝑟 / 2) ∈ ℝ+)
26 elrp 12048 . . . . . . . 8 ((𝑟 / 2) ∈ ℝ+ ↔ ((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)))
27 nnrecl 11557 . . . . . . . 8 (((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
2826, 27sylbi 208 . . . . . . 7 ((𝑟 / 2) ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
2925, 28syl 17 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
303ad2antrr 708 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐽 ∈ Top)
31 simpr1 1241 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴𝑋)
3231ad2antrr 708 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴𝑋)
331mopnuni 22459 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
3433ad3antrrr 712 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑋 = 𝐽)
3532, 34sseqtrd 3838 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 𝐽)
36 simplrr 787 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑢)
37 simplrl 786 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑢𝐽)
38 elunii 4635 . . . . . . . . . . . . 13 ((𝑧𝑢𝑢𝐽) → 𝑧 𝐽)
3936, 37, 38syl2anc 575 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 𝐽)
4039, 34eleqtrrd 2888 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑋)
41 simpr3 1245 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ((cls‘𝐽)‘𝐴) = 𝑋)
4241ad2antrr 708 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((cls‘𝐽)‘𝐴) = 𝑋)
4340, 42eleqtrrd 2888 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
4419adantr 468 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐷 ∈ (∞Met‘𝑋))
45 simprrl 790 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℕ)
4645nnrpd 12084 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℝ+)
4746rpreccld 12096 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ+)
4847rpxrd 12087 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ*)
491blopn 22518 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ*) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
5044, 40, 48, 49syl3anc 1483 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
51 blcntr 22431 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ+) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
5244, 40, 47, 51syl3anc 1483 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
53 eqid 2806 . . . . . . . . . . 11 𝐽 = 𝐽
5453clsndisj 21093 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐴 𝐽𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
5530, 35, 43, 50, 52, 54syl32anc 1490 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
56 n0 4132 . . . . . . . . 9 (((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
5755, 56sylib 209 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
5845adantr 468 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑛 ∈ ℕ)
59 inss2 4030 . . . . . . . . . . . 12 ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ⊆ 𝐴
60 simpr 473 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
6159, 60sseldi 3796 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝐴)
62 eqidd 2807 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
63 oveq2 6882 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (1 / 𝑥) = (1 / 𝑛))
6463oveq2d 6890 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝑦(ball‘𝐷)(1 / 𝑥)) = (𝑦(ball‘𝐷)(1 / 𝑛)))
6564eqeq2d 2816 . . . . . . . . . . . 12 (𝑥 = 𝑛 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛))))
66 oveq1 6881 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (𝑦(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
6766eqeq2d 2816 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))))
6865, 67rspc2ev 3517 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑡𝐴 ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))) → ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
6958, 61, 62, 68syl3anc 1483 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
70 ovex 6906 . . . . . . . . . . 11 (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ V
71 eqeq1 2810 . . . . . . . . . . . 12 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
72712rexbidv 3245 . . . . . . . . . . 11 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
7315rnmpt2 7000 . . . . . . . . . . 11 ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = {𝑧 ∣ ∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥))}
7470, 72, 73elab2 3549 . . . . . . . . . 10 ((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
7569, 74sylibr 225 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
76 inss1 4029 . . . . . . . . . . 11 ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ⊆ (𝑧(ball‘𝐷)(1 / 𝑛))
7776, 60sseldi 3796 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
7844adantr 468 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
7948adantr 468 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ∈ ℝ*)
8040adantr 468 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧𝑋)
8132adantr 468 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐴𝑋)
8281, 61sseldd 3799 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝑋)
83 blcom 22412 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ (1 / 𝑛) ∈ ℝ*) ∧ (𝑧𝑋𝑡𝑋)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
8478, 79, 80, 82, 83syl22anc 858 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
8577, 84mpbid 223 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)))
86 simprll 788 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑟 ∈ ℝ+)
8786adantr 468 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ+)
8887rphalfcld 12098 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ+)
8988rpxrd 12087 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ*)
90 simprrr 791 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) < (𝑟 / 2))
9186rphalfcld 12098 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ+)
92 rpre 12053 . . . . . . . . . . . . . . 15 ((1 / 𝑛) ∈ ℝ+ → (1 / 𝑛) ∈ ℝ)
93 rpre 12053 . . . . . . . . . . . . . . 15 ((𝑟 / 2) ∈ ℝ+ → (𝑟 / 2) ∈ ℝ)
94 ltle 10411 . . . . . . . . . . . . . . 15 (((1 / 𝑛) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9592, 93, 94syl2an 585 . . . . . . . . . . . . . 14 (((1 / 𝑛) ∈ ℝ+ ∧ (𝑟 / 2) ∈ ℝ+) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9647, 91, 95syl2anc 575 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9790, 96mpd 15 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ≤ (𝑟 / 2))
9897adantr 468 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ≤ (𝑟 / 2))
99 ssbl 22441 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋) ∧ ((1 / 𝑛) ∈ ℝ* ∧ (𝑟 / 2) ∈ ℝ*) ∧ (1 / 𝑛) ≤ (𝑟 / 2)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
10078, 82, 79, 89, 98, 99syl221anc 1493 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
10187rpred 12086 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ)
102100, 85sseldd 3799 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))
103 blhalf 22423 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋) ∧ (𝑟 ∈ ℝ ∧ 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
10478, 82, 101, 102, 103syl22anc 858 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
105 simprlr 789 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
106105adantr 468 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
107104, 106sstrd 3808 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ 𝑢)
108100, 107sstrd 3808 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)
109 eleq2 2874 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧𝑤𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
110 sseq1 3823 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑤𝑢 ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢))
111109, 110anbi12d 618 . . . . . . . . . 10 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → ((𝑧𝑤𝑤𝑢) ↔ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)))
112111rspcev 3502 . . . . . . . . 9 (((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∧ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11375, 85, 108, 112syl12anc 856 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11457, 113exlimddv 2026 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
115114anassrs 455 . . . . . 6 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11629, 115rexlimddv 3223 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11723, 116rexlimddv 3223 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
118117ralrimivva 3159 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
119 basgen2 21007 . . 3 ((𝐽 ∈ Top ∧ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽 ∧ ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
1203, 18, 118, 119syl3anc 1483 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
121120, 3eqeltrd 2885 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
122 tgclb 20988 . . . 4 (ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
123121, 122sylibr 225 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases)
124 omelon 8790 . . . . . 6 ω ∈ On
125 simpr2 1243 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ≼ ω)
126 nnex 11311 . . . . . . . . 9 ℕ ∈ V
127126xpdom2 8294 . . . . . . . 8 (𝐴 ≼ ω → (ℕ × 𝐴) ≼ (ℕ × ω))
128125, 127syl 17 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ (ℕ × ω))
129 nnenom 13003 . . . . . . . . 9 ℕ ≈ ω
130 omex 8787 . . . . . . . . . 10 ω ∈ V
131130enref 8225 . . . . . . . . 9 ω ≈ ω
132 xpen 8362 . . . . . . . . 9 ((ℕ ≈ ω ∧ ω ≈ ω) → (ℕ × ω) ≈ (ω × ω))
133129, 131, 132mp2an 675 . . . . . . . 8 (ℕ × ω) ≈ (ω × ω)
134 xpomen 9121 . . . . . . . 8 (ω × ω) ≈ ω
135133, 134entri 8246 . . . . . . 7 (ℕ × ω) ≈ ω
136 domentr 8251 . . . . . . 7 (((ℕ × 𝐴) ≼ (ℕ × ω) ∧ (ℕ × ω) ≈ ω) → (ℕ × 𝐴) ≼ ω)
137128, 135, 136sylancl 576 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ ω)
138 ondomen 9143 . . . . . 6 ((ω ∈ On ∧ (ℕ × 𝐴) ≼ ω) → (ℕ × 𝐴) ∈ dom card)
139124, 137, 138sylancr 577 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ∈ dom card)
14017ffnd 6257 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
141 dffn4 6337 . . . . . 6 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴) ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
142140, 141sylib 209 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
143 fodomnum 9163 . . . . 5 ((ℕ × 𝐴) ∈ dom card → ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴)))
144139, 142, 143sylc 65 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴))
145 domtr 8245 . . . 4 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴) ∧ (ℕ × 𝐴) ≼ ω) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
146144, 137, 145syl2anc 575 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
147 2ndci 21465 . . 3 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ∧ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2nd𝜔)
148123, 146, 147syl2anc 575 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2nd𝜔)
149120, 148eqeltrrd 2886 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2nd𝜔)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2156  wne 2978  wral 3096  wrex 3097  cin 3768  wss 3769  c0 4116   cuni 4630   class class class wbr 4844   × cxp 5309  dom cdm 5311  ran crn 5312  Oncon0 5936   Fn wfn 6096  wf 6097  ontowfo 6099  cfv 6101  (class class class)co 6874  cmpt2 6876  ωcom 7295  cen 8189  cdom 8190  cardccrd 9044  cr 10220  0cc0 10221  1c1 10222  *cxr 10358   < clt 10359  cle 10360   / cdiv 10969  cn 11305  2c2 11356  +crp 12046  topGenctg 16303  ∞Metcxmt 19939  ballcbl 19941  MetOpencmopn 19944  Topctop 20911  TopBasesctb 20963  clsccl 21036  2nd𝜔c2ndc 21455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-inf2 8785  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-isom 6110  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-map 8094  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-sup 8587  df-inf 8588  df-oi 8654  df-card 9048  df-acn 9051  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-n0 11560  df-z 11644  df-uz 11905  df-q 12008  df-rp 12047  df-xneg 12162  df-xadd 12163  df-xmul 12164  df-topgen 16309  df-psmet 19946  df-xmet 19947  df-bl 19949  df-mopn 19950  df-top 20912  df-topon 20929  df-bases 20964  df-cld 21037  df-ntr 21038  df-cls 21039  df-2ndc 21457
This theorem is referenced by:  met2ndc  22541
  Copyright terms: Public domain W3C validator