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 24443

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 24361	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
3	2	adantr 480	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ Top)
4		simpll 766	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝐷 ∈ (∞Met‘𝑋))
5		simplr1 1216	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝐴 ⊆ 𝑋)
6		simprr 772	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴)
7	5, 6	sseldd 3930	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝑋)
8		simprl 770	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ℕ)
9	8	nnrpd 12938	. . . . . . . . 9 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ℝ⁺)
10	9	rpreccld 12950	. . . . . . . 8 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (1 / 𝑥) ∈ ℝ⁺)
11	10	rpxrd 12941	. . . . . . 7 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (1 / 𝑥) ∈ ℝ^*)
12	1	blopn 24421	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (1 / 𝑥) ∈ ℝ^*) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
13	4, 7, 11, 12	syl3anc 1373	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑥 ∈ ℕ ∧ 𝑦 ∈ 𝐴)) → (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
14	13	ralrimivva 3175	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽)
15		eqid 2731	. . . . . 6 ⊢ (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))
16	15	fmpo 8006	. . . . 5 ⊢ (∀𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 (𝑦(ball‘𝐷)(1 / 𝑥)) ∈ 𝐽 ↔ (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
17	14, 16	sylib 218	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))):(ℕ × 𝐴)⟶𝐽)
18	17	frnd 6665	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽)
19		simpll 766	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → 𝐷 ∈ (∞Met‘𝑋))
20		simprl 770	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → 𝑢 ∈ 𝐽)
21		simprr 772	. . . . . 6 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → 𝑧 ∈ 𝑢)
22	1	mopni2 24414	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢) → ∃𝑟 ∈ ℝ⁺ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
23	19, 20, 21, 22	syl3anc 1373	. . . . 5 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → ∃𝑟 ∈ ℝ⁺ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
24		simprl 770	. . . . . . . 8 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → 𝑟 ∈ ℝ⁺)
25	24	rphalfcld 12952	. . . . . . 7 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → (𝑟 / 2) ∈ ℝ⁺)
26		elrp 12898	. . . . . . . 8 ⊢ ((𝑟 / 2) ∈ ℝ⁺ ↔ ((𝑟 / 2) ∈ ℝ ∧ 0 < (𝑟 / 2)))
27		nnrecl 12385	. . . . . . . 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 726	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐽 ∈ Top)
31		simpr1 1195	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ⊆ 𝑋)
32	31	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 ⊆ 𝑋)
33	1	mopnuni 24362	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
34	33	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑋 = ∪ 𝐽)
35	32, 34	sseqtrd 3966	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐴 ⊆ ∪ 𝐽)
36		simplrr 777	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ 𝑢)
37		simplrl 776	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑢 ∈ 𝐽)
38		elunii 4863	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑢 ∧ 𝑢 ∈ 𝐽) → 𝑧 ∈ ∪ 𝐽)
39	36, 37, 38	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ∪ 𝐽)
40	39, 34	eleqtrrd 2834	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ 𝑋)
41		simpr3 1197	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ((cls‘𝐽)‘𝐴) = 𝑋)
42	41	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((cls‘𝐽)‘𝐴) = 𝑋)
43	40, 42	eleqtrrd 2834	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
44	19	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝐷 ∈ (∞Met‘𝑋))
45		simprrl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℕ)
46	45	nnrpd 12938	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑛 ∈ ℝ⁺)
47	46	rpreccld 12950	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ⁺)
48	47	rpxrd 12941	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) ∈ ℝ^*)
49	1	blopn 24421	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ (1 / 𝑛) ∈ ℝ^*) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
50	44, 40, 48, 49	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽)
51		blcntr 24334	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ (1 / 𝑛) ∈ ℝ⁺) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
52	44, 40, 47, 51	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))
53		eqid 2731	. . . . . . . . . . 11 ⊢ ∪ 𝐽 = ∪ 𝐽
54	53	clsndisj 22996	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∈ 𝐽 ∧ 𝑧 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
55	30, 35, 43, 50, 52, 54	syl32anc 1380	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴) ≠ ∅)
56		n0 4302	. . . . . . . . 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 4154	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ 𝐴)
61		eqidd 2732	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
62		oveq2 7360	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑛 → (1 / 𝑥) = (1 / 𝑛))
63	62	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑛 → (𝑦(ball‘𝐷)(1 / 𝑥)) = (𝑦(ball‘𝐷)(1 / 𝑛)))
64	63	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑛 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛))))
65		oveq1 7359	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑡 → (𝑦(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛)))
66	65	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑡 → ((𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑛)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))))
67	64, 66	rspc2ev 3585	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ 𝑡 ∈ 𝐴 ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑡(ball‘𝐷)(1 / 𝑛))) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
68	58, 60, 61, 67	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥)))
69		ovex 7385	. . . . . . . . . . 11 ⊢ (𝑡(ball‘𝐷)(1 / 𝑛)) ∈ V
70		eqeq1 2735	. . . . . . . . . . . 12 ⊢ (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
71	70	2rexbidv 3197	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥)) ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 (𝑡(ball‘𝐷)(1 / 𝑛)) = (𝑦(ball‘𝐷)(1 / 𝑥))))
72	15	rnmpo 7485	. . . . . . . . . . 11 ⊢ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) = {𝑧 ∣ ∃𝑥 ∈ ℕ ∃𝑦 ∈ 𝐴 𝑧 = (𝑦(ball‘𝐷)(1 / 𝑥))}
73	69, 71, 72	elab2 3633	. . . . . . . . . 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 4153	. . . . . . . . . 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 3930	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑡 ∈ 𝑋)
81		blcom 24315	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (1 / 𝑛) ∈ ℝ^*) ∧ (𝑧 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋)) → (𝑡 ∈ (𝑧(ball‘𝐷)(1 / 𝑛)) ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
82	76, 77, 78, 80, 81	syl22anc 838	. . . . . . . . . 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 778	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → 𝑟 ∈ ℝ⁺)
85	84	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ⁺)
86	85	rphalfcld 12952	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ⁺)
87	86	rpxrd 12941	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑟 / 2) ∈ ℝ^*)
88		simprrr 781	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (1 / 𝑛) < (𝑟 / 2))
89	84	rphalfcld 12952	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑟 / 2) ∈ ℝ⁺)
90		rpre 12905	. . . . . . . . . . . . . . 15 ⊢ ((1 / 𝑛) ∈ ℝ⁺ → (1 / 𝑛) ∈ ℝ)
91		rpre 12905	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 / 2) ∈ ℝ⁺ → (𝑟 / 2) ∈ ℝ)
92		ltle 11207	. . . . . . . . . . . . . . 15 ⊢ (((1 / 𝑛) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
93	90, 91, 92	syl2an 596	. . . . . . . . . . . . . 14 ⊢ (((1 / 𝑛) ∈ ℝ⁺ ∧ (𝑟 / 2) ∈ ℝ⁺) → ((1 / 𝑛) < (𝑟 / 2) → (1 / 𝑛) ≤ (𝑟 / 2)))
94	47, 89, 93	syl2anc 584	. . . . . . . . . . . . 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 24344	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡 ∈ 𝑋) ∧ ((1 / 𝑛) ∈ ℝ^* ∧ (𝑟 / 2) ∈ ℝ^*) ∧ (1 / 𝑛) ≤ (𝑟 / 2)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
98	76, 80, 77, 87, 96, 97	syl221anc 1383	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ (𝑡(ball‘𝐷)(𝑟 / 2)))
99	85	rpred 12940	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑟 ∈ ℝ)
100	98, 83	sseldd 3930	. . . . . . . . . . . 12 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))
101		blhalf 24326	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡 ∈ 𝑋) ∧ (𝑟 ∈ ℝ ∧ 𝑧 ∈ (𝑡(ball‘𝐷)(𝑟 / 2)))) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
102	76, 80, 99, 100, 101	syl22anc 838	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑧(ball‘𝐷)𝑟))
103		simprlr 779	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
104	103	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)
105	102, 104	sstrd 3940	. . . . . . . . . 10 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(𝑟 / 2)) ⊆ 𝑢)
106	98, 105	sstrd 3940	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)
107		eleq2 2820	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛))))
108		sseq1 3955	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → (𝑤 ⊆ 𝑢 ↔ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢))
109	107, 108	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑤 = (𝑡(ball‘𝐷)(1 / 𝑛)) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢) ↔ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)))
110	109	rspcev 3572	. . . . . . . . 9 ⊢ (((𝑡(ball‘𝐷)(1 / 𝑛)) ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∧ (𝑧 ∈ (𝑡(ball‘𝐷)(1 / 𝑛)) ∧ (𝑡(ball‘𝐷)(1 / 𝑛)) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
111	74, 83, 106, 110	syl12anc 836	. . . . . . . 8 ⊢ (((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ ((𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢) ∧ (𝑛 ∈ ℕ ∧ (1 / 𝑛) < (𝑟 / 2)))) ∧ 𝑡 ∈ ((𝑧(ball‘𝐷)(1 / 𝑛)) ∩ 𝐴)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
112	57, 111	exlimddv 1936	. . . . . . 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 3139	. . . . 5 ⊢ ((((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) ∧ (𝑟 ∈ ℝ⁺ ∧ (𝑧(ball‘𝐷)𝑟) ⊆ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
115	23, 114	rexlimddv 3139	. . . 4 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑧 ∈ 𝑢)) → ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
116	115	ralrimivva 3175	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ∀𝑢 ∈ 𝐽 ∀𝑧 ∈ 𝑢 ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢))
117		basgen2 22910	. . 3 ⊢ ((𝐽 ∈ Top ∧ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ⊆ 𝐽 ∧ ∀𝑢 ∈ 𝐽 ∀𝑧 ∈ 𝑢 ∃𝑤 ∈ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑢)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
118	3, 18, 116, 117	syl3anc 1373	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) = 𝐽)
119	118, 3	eqeltrd 2831	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
120		tgclb 22891	. . . 4 ⊢ (ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ↔ (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ Top)
121	119, 120	sylibr 234	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases)
122		omelon 9542	. . . . . 6 ⊢ ω ∈ On
123		simpr2 1196	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐴 ≼ ω)
124		nnex 12137	. . . . . . . . 9 ⊢ ℕ ∈ V
125	124	xpdom2 8991	. . . . . . . 8 ⊢ (𝐴 ≼ ω → (ℕ × 𝐴) ≼ (ℕ × ω))
126	123, 125	syl 17	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ (ℕ × ω))
127		nnenom 13893	. . . . . . . . 9 ⊢ ℕ ≈ ω
128		omex 9539	. . . . . . . . . 10 ⊢ ω ∈ V
129	128	enref 8913	. . . . . . . . 9 ⊢ ω ≈ ω
130		xpen 9059	. . . . . . . . 9 ⊢ ((ℕ ≈ ω ∧ ω ≈ ω) → (ℕ × ω) ≈ (ω × ω))
131	127, 129, 130	mp2an 692	. . . . . . . 8 ⊢ (ℕ × ω) ≈ (ω × ω)
132		xpomen 9912	. . . . . . . 8 ⊢ (ω × ω) ≈ ω
133	131, 132	entri 8936	. . . . . . 7 ⊢ (ℕ × ω) ≈ ω
134		domentr 8941	. . . . . . 7 ⊢ (((ℕ × 𝐴) ≼ (ℕ × ω) ∧ (ℕ × ω) ≈ ω) → (ℕ × 𝐴) ≼ ω)
135	126, 133, 134	sylancl 586	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ≼ ω)
136		ondomen 9934	. . . . . 6 ⊢ ((ω ∈ On ∧ (ℕ × 𝐴) ≼ ω) → (ℕ × 𝐴) ∈ dom card)
137	122, 135, 136	sylancr 587	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (ℕ × 𝐴) ∈ dom card)
138	17	ffnd 6658	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) Fn (ℕ × 𝐴))
139		dffn4 6747	. . . . . 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 9954	. . . . 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 8935	. . . 4 ⊢ ((ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ (ℕ × 𝐴) ∧ (ℕ × 𝐴) ≼ ω) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
144	142, 135, 143	syl2anc 584	. . 3 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω)
145		2ndci 23369	. . 3 ⊢ ((ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ∈ TopBases ∧ ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥))) ≼ ω) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2^ndω)
146	121, 144, 145	syl2anc 584	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → (topGen‘ran (𝑥 ∈ ℕ, 𝑦 ∈ 𝐴 ↦ (𝑦(ball‘𝐷)(1 / 𝑥)))) ∈ 2^ndω)
147	118, 146	eqeltrrd 2832	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2^ndω)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 ∩ cin 3896 ⊆ wss 3897 ∅c0 4282 ∪ cuni 4858 class class class wbr 5093 × cxp 5617 dom cdm 5619 ran crn 5620 Oncon0 6312 Fn wfn 6482 ⟶wf 6483 –onto→wfo 6485 ‘cfv 6487 (class class class)co 7352 ∈ cmpo 7354 ωcom 7802 ≈ cen 8872 ≼ cdom 8873 cardccrd 9834 ℝcr 11011 0cc0 11012 1c1 11013 ℝ^*cxr 11151 < clt 11152 ≤ cle 11153 / cdiv 11780 ℕcn 12131 2c2 12186 ℝ⁺crp 12896 topGenctg 17347 ∞Metcxmet 21282 ballcbl 21284 MetOpencmopn 21287 Topctop 22814 TopBasesctb 22866 clsccl 22939 2^ndωc2ndc 23359

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 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-inf2 9537 ax-cnex 11068 ax-resscn 11069 ax-1cn 11070 ax-icn 11071 ax-addcl 11072 ax-addrcl 11073 ax-mulcl 11074 ax-mulrcl 11075 ax-mulcom 11076 ax-addass 11077 ax-mulass 11078 ax-distr 11079 ax-i2m1 11080 ax-1ne0 11081 ax-1rid 11082 ax-rnegex 11083 ax-rrecex 11084 ax-cnre 11085 ax-pre-lttri 11086 ax-pre-lttrn 11087 ax-pre-ltadd 11088 ax-pre-mulgt0 11089 ax-pre-sup 11090

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-iin 4944 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-er 8628 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9838 df-acn 9841 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 df-sub 11352 df-neg 11353 df-div 11781 df-nn 12132 df-2 12194 df-n0 12388 df-z 12475 df-uz 12739 df-q 12853 df-rp 12897 df-xneg 13017 df-xadd 13018 df-xmul 13019 df-topgen 17353 df-psmet 21289 df-xmet 21290 df-bl 21292 df-mopn 21293 df-top 22815 df-topon 22832 df-bases 22867 df-cld 22940 df-ntr 22941 df-cls 22942 df-2ndc 23361

This theorem is referenced by: met2ndc 24444

W3C validator