met2ndci - Metamath Proof Explorer

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

Theorem met2ndci 24465

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‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2^ndω)

Proof of Theorem met2ndci Dummy variables 𝑛 𝑟 𝑡 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		methaus.1	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
2	1	mopntop 24383	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
3	2	adantr 480	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ Top)
4		simpll 767	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
5		simplr1 1217	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝐴 ⊆ 𝑋)
6		simprr 773	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
7	5, 6	sseldd 3923	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝑋)
8		simprl 771	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ℕ)
9	8	nnrpd 12948	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ℝ⁺)
10	9	rpreccld 12960	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (1 / 𝑥) ∈ ℝ⁺)
11	10	rpxrd 12951	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (1 / 𝑥) ∈ ℝ^*)
12	1	blopn 24443	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (1 / 𝑥) ∈ ℝ^*) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
13	4, 7, 11, 12	syl3anc 1374	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
14	13	ralrimivva 3181	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
15		eqid 2737	. . . . . 6 ⊢ (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))
16	15	fmpo 8012	. . . . 5 ⊢ (∀𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽 ↔ (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
17	14, 16	sylib 218	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
18	17	frnd 6668	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽)
19		simpll 767	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → 𝐷 ∈ (∞Met‘𝑋))
20		simprl 771	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → 𝑢 ∈ 𝐽)
21		simprr 773	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → 𝑧 ∈ 𝑢)
22	1	mopni2 24436	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢) → ∃𝑟 ∈ ℝ⁺ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
23	19, 20, 21, 22	syl3anc 1374	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → ∃𝑟 ∈ ℝ⁺ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
24		simprl 771	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ⁺)
25	24	rphalfcld 12962	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → (𝑟 / 2) ∈ ℝ⁺)
26		elrp 12908	. . . . . . . 8 ⊢ ((𝑟 / 2) ∈ ℝ⁺ ↔ ((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)))
27		nnrecl 12400	. . . . . . . 8 ⊢ (((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
28	26, 27	sylbi 217	. . . . . . 7 ⊢ ((𝑟 / 2) ∈ ℝ⁺ → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
29	25, 28	syl 17	. . . . . 6 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑛 ∈ ℕ (1 / 𝑛) < (𝑟 / 2))
30	3	ad2antrr 727	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐽 ∈ Top)
31		simpr1 1196	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ⊆ 𝑋)
32	31	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 ⊆ 𝑋)
33	1	mopnuni 24384	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
34	33	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑋 = ∪ 𝐽)
35	32, 34	sseqtrd 3959	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 ⊆ ∪ 𝐽)
36		simplrr 778	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ 𝑢)
37		simplrl 777	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑢 ∈ 𝐽)
38		elunii 4856	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝐽) → 𝑧 ∈ ∪ 𝐽)
39	36, 37, 38	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ∪ 𝐽)
40	39, 34	eleqtrrd 2840	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ 𝑋)
41		simpr3 1198	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ((cls‘𝐽)‘𝐴) = 𝑋)
42	41	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((cls‘𝐽)‘𝐴) = 𝑋)
43	40, 42	eleqtrrd 2840	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
44	19	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐷 ∈ (∞Met‘𝑋))
45		simprrl 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℕ)
46	45	nnrpd 12948	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℝ⁺)
47	46	rpreccld 12960	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ⁺)
48	47	rpxrd 12951	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ^*)
49	1	blopn 24443	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ (1 / 𝑛) ∈ ℝ^*) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
50	44, 40, 48, 49	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
51		blcntr 24356	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ (1 / 𝑛) ∈ ℝ⁺) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
52	44, 40, 47, 51	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
53		eqid 2737	. . . . . . . . . . 11 ⊢ ∪ 𝐽 = ∪ 𝐽
54	53	clsndisj 23018	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽 ∧ 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
55	30, 35, 43, 50, 52, 54	syl32anc 1381	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
56		n0 4294	. . . . . . . . 9 ⊢ (((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
57	55, 56	sylib 218	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑡 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
58	45	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑛 ∈ ℕ)
59		simpr 484	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴))
60	59	elin2d 4146	. . . . . . . . . . 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 7366	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (1 / 𝑥) = (1 / 𝑛))
63	62	oveq2d 7374	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑦(ball‘𝐷)(1 / 𝑥)) = (𝑦(ball‘𝐷)(1 / 𝑛)))
64	63	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛))))
65		oveq1 7365	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑡 → (𝑦(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
66	65	eqeq2d 2748	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑡 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))))
67	64, 66	rspc2ev 3578	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ 𝑡 ∈ 𝐴 ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
68	58, 60, 61, 67	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
69		ovex 7391	. . . . . . . . . . 11 ⊢ (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ V
70		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
71	70	2rexbidv 3203	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
72	15	rnmpo 7491	. . . . . . . . . . 11 ⊢ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = {𝑧 ∣ ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥))}
73	69, 71, 72	elab2 3626	. . . . . . . . . 10 ⊢ ((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
74	68, 73	sylibr 234	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
75	59	elin1d 4145	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
76	44	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
77	48	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ∈ ℝ^*)
78	40	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ 𝑋)
79	32	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝐴 ⊆ 𝑋)
80	79, 60	sseldd 3923	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ 𝑋)
81		blcom 24337	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (1 / 𝑛) ∈ ℝ^*) ∧ (𝑧 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
82	76, 77, 78, 80, 81	syl22anc 839	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
83	75, 82	mpbid 232	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)))
84		simprll 779	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑟 ∈ ℝ⁺)
85	84	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ⁺)
86	85	rphalfcld 12962	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ⁺)
87	86	rpxrd 12951	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ^*)
88		simprrr 782	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) < (𝑟 / 2))
89	84	rphalfcld 12962	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ⁺)
90		rpre 12915	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑛) ∈ ℝ⁺ → (1 / 𝑛) ∈ ℝ)
91		rpre 12915	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 / 2) ∈ ℝ⁺ → (𝑟 / 2) ∈ ℝ)
92		ltle 11222	. . . . . . . . . . . . . . 15 ⊢ (((1 / 𝑛) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
93	90, 91, 92	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((1 / 𝑛) ∈ ℝ⁺ ∧ (𝑟 / 2) ∈ ℝ⁺) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
94	47, 89, 93	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
95	88, 94	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ≤ (𝑟 / 2))
96	95	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (1 / 𝑛) ≤ (𝑟 / 2))
97		ssbl 24366	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡 ∈ 𝑋) ∧ ((1 / 𝑛) ∈ ℝ^* ∧ (𝑟 / 2) ∈ ℝ^*) ∧ (1 / 𝑛) ≤ (𝑟 / 2)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
98	76, 80, 77, 87, 96, 97	syl221anc 1384	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
99	85	rpred 12950	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ)
100	98, 83	sseldd 3923	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))
101		blhalf 24348	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡 ∈ 𝑋) ∧ (𝑟 ∈ ℝ ∧ 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
102	76, 80, 99, 100, 101	syl22anc 839	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
103		simprlr 780	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
104	103	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
105	102, 104	sstrd 3933	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ 𝑢)
106	98, 105	sstrd 3933	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)
107		eleq2 2826	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
108		sseq1 3948	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑤 ⊆ 𝑢 ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢))
109	107, 108	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢) ↔ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)))
110	109	rspcev 3565	. . . . . . . . 9 ⊢ (((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∧ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
111	74, 83, 106, 110	syl12anc 837	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
112	57, 111	exlimddv 1937	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
113	112	anassrs 467	. . . . . 6 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2))) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
114	29, 113	rexlimddv 3145	. . . . 5 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
115	23, 114	rexlimddv 3145	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
116	115	ralrimivva 3181	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑢 ∈ 𝐽 ∀𝑧 ∈ 𝑢 ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
117		basgen2 22932	. . 3 ⊢ ((𝐽 ∈ Top ∧ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽 ∧ ∀𝑢 ∈ 𝐽 ∀𝑧 ∈ 𝑢 ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
118	3, 18, 116, 117	syl3anc 1374	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
119	118, 3	eqeltrd 2837	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
120		tgclb 22913	. . . 4 ⊢ (ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
121	119, 120	sylibr 234	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases)
122		omelon 9556	. . . . . 6 ⊢ ω ∈ On
123		simpr2 1197	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ≼ ω)
124		nnex 12152	. . . . . . . . 9 ⊢ ℕ ∈ V
125	124	xpdom2 9001	. . . . . . . 8 ⊢ (𝐴 ≼ ω → (ℕ × 𝐴) ≼ (ℕ × ω))
126	123, 125	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ (ℕ × ω))
127		nnenom 13904	. . . . . . . . 9 ⊢ ℕ ≈ ω
128		omex 9553	. . . . . . . . . 10 ⊢ ω ∈ V
129	128	enref 8923	. . . . . . . . 9 ⊢ ω ≈ ω
130		xpen 9069	. . . . . . . . 9 ⊢ ((ℕ ≈ ω ∧ ω ≈ ω) → (ℕ × ω) ≈ (ω × ω))
131	127, 129, 130	mp2an 693	. . . . . . . 8 ⊢ (ℕ × ω) ≈ (ω × ω)
132		xpomen 9926	. . . . . . . 8 ⊢ (ω × ω) ≈ ω
133	131, 132	entri 8946	. . . . . . 7 ⊢ (ℕ × ω) ≈ ω
134		domentr 8951	. . . . . . 7 ⊢ (((ℕ × 𝐴) ≼ (ℕ × ω) ∧ (ℕ × ω) ≈ ω) → (ℕ × 𝐴) ≼ ω)
135	126, 133, 134	sylancl 587	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ ω)
136		ondomen 9948	. . . . . 6 ⊢ ((ω ∈ On ∧ (ℕ × 𝐴) ≼ ω) → (ℕ × 𝐴) ∈ dom card)
137	122, 135, 136	sylancr 588	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ∈ dom card)
138	17	ffnd 6661	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
139		dffn4 6750	. . . . . 6 ⊢ ((𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴) ↔ (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
140	138, 139	sylib 218	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))))
141		fodomnum 9968	. . . . 5 ⊢ ((ℕ × 𝐴) ∈ dom card → ((𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)–onto→ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴)))
142	137, 140, 141	sylc 65	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴))
143		domtr 8945	. . . 4 ⊢ ((ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴) ∧ (ℕ × 𝐴) ≼ ω) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
144	142, 135, 143	syl2anc 585	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
145		2ndci 23391	. . 3 ⊢ ((ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ∧ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2^ndω)
146	121, 144, 145	syl2anc 585	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2^ndω)
147	118, 146	eqeltrrd 2838	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2^ndω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 ∪ cuni 4851 class class class wbr 5086 × cxp 5620 dom cdm 5622 ran crn 5623 Oncon0 6315 Fn wfn 6485 ⟶wf 6486 –onto→wfo 6488 ‘cfv 6490 (class class class)co 7358 ∈ cmpo 7360 ωcom 7808 ≈ cen 8881 ≼ cdom 8882 cardccrd 9848 ℝcr 11026 0cc0 11027 1c1 11028 ℝ^*cxr 11166 < clt 11167 ≤ cle 11168 / cdiv 11795 ℕcn 12146 2c2 12201 ℝ⁺crp 12906 topGenctg 17358 ∞Metcxmet 21296 ballcbl 21298 MetOpencmopn 21301 Topctop 22836 TopBasesctb 22888 clsccl 22961 2^ndωc2ndc 23381

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-inf2 9551 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-er 8634 df-map 8766 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-sup 9346 df-inf 9347 df-oi 9416 df-card 9852 df-acn 9855 df-pnf 11169 df-mnf 11170 df-xr 11171 df-ltxr 11172 df-le 11173 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-n0 12403 df-z 12490 df-uz 12753 df-q 12863 df-rp 12907 df-xneg 13027 df-xadd 13028 df-xmul 13029 df-topgen 17364 df-psmet 21303 df-xmet 21304 df-bl 21306 df-mopn 21307 df-top 22837 df-topon 22854 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-2ndc 23383

This theorem is referenced by: met2ndc 24466

W3C validator