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

Theorem met2ndci 23749
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 23664 . . . 4 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
32adantr 481 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ Top)
4 simpll 764 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
5 simplr1 1214 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝐴𝑋)
6 simprr 770 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝐴)
75, 6sseldd 3931 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑦𝑋)
8 simprl 768 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℕ)
98nnrpd 12840 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → 𝑥 ∈ ℝ+)
109rpreccld 12852 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ+)
1110rpxrd 12843 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (1 / 𝑥) ∈ ℝ*)
121blopn 23727 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (1 / 𝑥) ∈ ℝ*) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
134, 7, 11, 12syl3anc 1370 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦𝐴)) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
1413ralrimivva 3194 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
15 eqid 2737 . . . . . 6 (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))
1615fmpo 7951 . . . . 5 (∀𝑥 ∈ ℕ ∀𝑦𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽 ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
1714, 16sylib 217 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
1817frnd 6643 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽)
19 simpll 764 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝐷 ∈ (∞Met‘𝑋))
20 simprl 768 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝑢𝐽)
21 simprr 770 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → 𝑧𝑢)
221mopni2 23720 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢𝐽𝑧𝑢) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
2319, 20, 21, 22syl3anc 1370 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑟 ∈ ℝ+ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
24 simprl 768 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ+)
2524rphalfcld 12854 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → (𝑟 / 2) ∈ ℝ+)
26 elrp 12802 . . . . . . . 8 ((𝑟 / 2) ∈ ℝ+ ↔ ((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)))
27 nnrecl 12301 . . . . . . . 8 (((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
2826, 27sylbi 216 . . . . . . 7 ((𝑟 / 2) ∈ ℝ+ → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
2925, 28syl 17 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
303ad2antrr 723 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐽 ∈ Top)
31 simpr1 1193 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴𝑋)
3231ad2antrr 723 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴𝑋)
331mopnuni 23665 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
3433ad3antrrr 727 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑋 = 𝐽)
3532, 34sseqtrd 3970 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 𝐽)
36 simplrr 775 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑢)
37 simplrl 774 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑢𝐽)
38 elunii 4853 . . . . . . . . . . . . 13 ((𝑧𝑢𝑢𝐽) → 𝑧 𝐽)
3936, 37, 38syl2anc 584 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 𝐽)
4039, 34eleqtrrd 2841 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧𝑋)
41 simpr3 1195 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ((cls‘𝐽)‘𝐴) = 𝑋)
4241ad2antrr 723 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((cls‘𝐽)‘𝐴) = 𝑋)
4340, 42eleqtrrd 2841 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
4419adantr 481 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐷 ∈ (∞Met‘𝑋))
45 simprrl 778 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℕ)
4645nnrpd 12840 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℝ+)
4746rpreccld 12852 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ+)
4847rpxrd 12843 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ*)
491blopn 23727 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ*) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
5044, 40, 48, 49syl3anc 1370 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
51 blcntr 23637 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋 ∧ (1 / 𝑛) ∈ ℝ+) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
5244, 40, 47, 51syl3anc 1370 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
53 eqid 2737 . . . . . . . . . . 11 𝐽 = 𝐽
5453clsndisj 22297 . . . . . . . . . 10 (((𝐽 ∈ Top ∧ 𝐴 𝐽𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
5530, 35, 43, 50, 52, 54syl32anc 1377 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
56 n0 4290 . . . . . . . . 9 (((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
5755, 56sylib 217 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
5845adantr 481 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑛 ∈ ℕ)
59 simpr 485 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
6059elin2d 4143 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝐴)
61 eqidd 2738 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
62 oveq2 7321 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (1 / 𝑥) = (1 / 𝑛))
6362oveq2d 7329 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝑦(ball‘𝐷)(1 / 𝑥)) = (𝑦(ball‘𝐷)(1 / 𝑛)))
6463eqeq2d 2748 . . . . . . . . . . . 12 (𝑥 = 𝑛 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛))))
65 oveq1 7320 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (𝑦(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
6665eqeq2d 2748 . . . . . . . . . . . 12 (𝑦 = 𝑡 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))))
6764, 66rspc2ev 3581 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑡𝐴 ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))) → ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
6858, 60, 61, 67syl3anc 1370 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
69 ovex 7346 . . . . . . . . . . 11 (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ V
70 eqeq1 2741 . . . . . . . . . . . 12 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
71702rexbidv 3210 . . . . . . . . . . 11 (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
7215rnmpo 7445 . . . . . . . . . . 11 ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = {𝑧 ∣ ∃𝑥 ∈ ℕ ∃𝑦𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥))}
7369, 71, 72elab2 3622 . . . . . . . . . 10 ((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ↔ ∃𝑥 ∈ ℕ ∃𝑦𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
7468, 73sylibr 233 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
7559elin1d 4142 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
7644adantr 481 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
7748adantr 481 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ∈ ℝ*)
7840adantr 481 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧𝑋)
7932adantr 481 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐴𝑋)
8079, 60sseldd 3931 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡𝑋)
81 blcom 23618 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ (1 / 𝑛) ∈ ℝ*) ∧ (𝑧𝑋𝑡𝑋)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
8276, 77, 78, 80, 81syl22anc 836 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
8375, 82mpbid 231 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)))
84 simprll 776 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑟 ∈ ℝ+)
8584adantr 481 . . . . . . . . . . . . 13 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ+)
8685rphalfcld 12854 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ+)
8786rpxrd 12843 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ*)
88 simprrr 779 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) < (𝑟 / 2))
8984rphalfcld 12854 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ+)
90 rpre 12808 . . . . . . . . . . . . . . 15 ((1 / 𝑛) ∈ ℝ+ → (1 / 𝑛) ∈ ℝ)
91 rpre 12808 . . . . . . . . . . . . . . 15 ((𝑟 / 2) ∈ ℝ+ → (𝑟 / 2) ∈ ℝ)
92 ltle 11133 . . . . . . . . . . . . . . 15 (((1 / 𝑛) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9390, 91, 92syl2an 596 . . . . . . . . . . . . . 14 (((1 / 𝑛) ∈ ℝ+ ∧ (𝑟 / 2) ∈ ℝ+) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9447, 89, 93syl2anc 584 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
9588, 94mpd 15 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ≤ (𝑟 / 2))
9695adantr 481 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ≤ (𝑟 / 2))
97 ssbl 23647 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋) ∧ ((1 / 𝑛) ∈ ℝ* ∧ (𝑟 / 2) ∈ ℝ*) ∧ (1 / 𝑛) ≤ (𝑟 / 2)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
9876, 80, 77, 87, 96, 97syl221anc 1380 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
9985rpred 12842 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ)
10098, 83sseldd 3931 . . . . . . . . . . . 12 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))
101 blhalf 23629 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋) ∧ (𝑟 ∈ ℝ ∧ 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
10276, 80, 99, 100, 101syl22anc 836 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
103 simprlr 777 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
104103adantr 481 . . . . . . . . . . 11 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
105102, 104sstrd 3940 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ 𝑢)
10698, 105sstrd 3940 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)
107 eleq2 2826 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧𝑤𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
108 sseq1 3955 . . . . . . . . . . 11 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑤𝑢 ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢))
109107, 108anbi12d 631 . . . . . . . . . 10 (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → ((𝑧𝑤𝑤𝑢) ↔ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)))
110109rspcev 3570 . . . . . . . . 9 (((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∧ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11174, 83, 106, 110syl12anc 834 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11257, 111exlimddv 1937 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ ((𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
113112anassrs 468 . . . . . 6 (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11429, 113rexlimddv 3155 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) ∧ (𝑟 ∈ ℝ+ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
11523, 114rexlimddv 3155 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢𝐽𝑧𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
116115ralrimivva 3194 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢))
117 basgen2 22210 . . 3 ((𝐽 ∈ Top ∧ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽 ∧ ∀𝑢𝐽𝑧𝑢𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧𝑤𝑤𝑢)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
1183, 18, 116, 117syl3anc 1370 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
119118, 3eqeltrd 2838 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
120 tgclb 22191 . . . 4 (ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
121119, 120sylibr 233 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases)
122 omelon 9472 . . . . . 6 ω ∈ On
123 simpr2 1194 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ≼ ω)
124 nnex 12049 . . . . . . . . 9 ℕ ∈ V
125124xpdom2 8907 . . . . . . . 8 (𝐴 ≼ ω → (ℕ × 𝐴) ≼ (ℕ × ω))
126123, 125syl 17 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ (ℕ × ω))
127 nnenom 13770 . . . . . . . . 9 ℕ ≈ ω
128 omex 9469 . . . . . . . . . 10 ω ∈ V
129128enref 8821 . . . . . . . . 9 ω ≈ ω
130 xpen 8980 . . . . . . . . 9 ((ℕ ≈ ω ∧ ω ≈ ω) → (ℕ × ω) ≈ (ω × ω))
131127, 129, 130mp2an 689 . . . . . . . 8 (ℕ × ω) ≈ (ω × ω)
132 xpomen 9841 . . . . . . . 8 (ω × ω) ≈ ω
133131, 132entri 8844 . . . . . . 7 (ℕ × ω) ≈ ω
134 domentr 8849 . . . . . . 7 (((ℕ × 𝐴) ≼ (ℕ × ω) ∧ (ℕ × ω) ≈ ω) → (ℕ × 𝐴) ≼ ω)
135126, 133, 134sylancl 586 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ ω)
136 ondomen 9863 . . . . . 6 ((ω ∈ On ∧ (ℕ × 𝐴) ≼ ω) → (ℕ × 𝐴) ∈ dom card)
137122, 135, 136sylancr 587 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ∈ dom card)
13817ffnd 6636 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
139 dffn4 6729 . . . . . 6 ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴) ↔ (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
140138, 139sylib 217 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
141 fodomnum 9883 . . . . 5 ((ℕ × 𝐴) ∈ dom card → ((𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴)))
142137, 140, 141sylc 65 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴))
143 domtr 8843 . . . 4 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴) ∧ (ℕ × 𝐴) ≼ ω) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
144142, 135, 143syl2anc 584 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
145 2ndci 22670 . . 3 ((ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ∧ ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2ndω)
146121, 144, 145syl2anc 584 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2ndω)
147118, 146eqeltrrd 2839 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴𝑋𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2ndω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2941  wral 3062  wrex 3071  cin 3895  wss 3896  c0 4266   cuni 4848   class class class wbr 5085   × cxp 5603  dom cdm 5605  ran crn 5606  Oncon0 6286   Fn wfn 6458  wf 6459  ontowfo 6461  cfv 6463  (class class class)co 7313  cmpo 7315  ωcom 7755  cen 8776  cdom 8777  cardccrd 9761  cr 10940  0cc0 10941  1c1 10942  *cxr 11078   < clt 11079  cle 11080   / cdiv 11702  cn 12043  2c2 12098  +crp 12800  topGenctg 17215  ∞Metcxmet 20653  ballcbl 20655  MetOpencmopn 20658  Topctop 22113  TopBasesctb 22166  clsccl 22240  2ndωc2ndc 22660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5222  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-inf2 9467  ax-cnex 10997  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-mulcom 11005  ax-addass 11006  ax-mulass 11007  ax-distr 11008  ax-i2m1 11009  ax-1ne0 11010  ax-1rid 11011  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016  ax-pre-ltadd 11017  ax-pre-mulgt0 11018  ax-pre-sup 11019
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-int 4891  df-iun 4937  df-iin 4938  df-br 5086  df-opab 5148  df-mpt 5169  df-tr 5203  df-id 5505  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5560  df-se 5561  df-we 5562  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-pred 6222  df-ord 6289  df-on 6290  df-lim 6291  df-suc 6292  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-isom 6472  df-riota 7270  df-ov 7316  df-oprab 7317  df-mpo 7318  df-om 7756  df-1st 7874  df-2nd 7875  df-frecs 8142  df-wrecs 8173  df-recs 8247  df-rdg 8286  df-1o 8342  df-er 8544  df-map 8663  df-en 8780  df-dom 8781  df-sdom 8782  df-fin 8783  df-sup 9269  df-inf 9270  df-oi 9337  df-card 9765  df-acn 9768  df-pnf 11081  df-mnf 11082  df-xr 11083  df-ltxr 11084  df-le 11085  df-sub 11277  df-neg 11278  df-div 11703  df-nn 12044  df-2 12106  df-n0 12304  df-z 12390  df-uz 12653  df-q 12759  df-rp 12801  df-xneg 12918  df-xadd 12919  df-xmul 12920  df-topgen 17221  df-psmet 20660  df-xmet 20661  df-bl 20663  df-mopn 20664  df-top 22114  df-topon 22131  df-bases 22167  df-cld 22241  df-ntr 22242  df-cls 22243  df-2ndc 22662
This theorem is referenced by:  met2ndc  23750
  Copyright terms: Public domain W3C validator