met2ndci

Description: A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015)

		Ref	Expression
	Hypothesis	methaus.1	$⊢ J = MetOpen (D)$
	Assertion	met2ndci	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to J \in 2^{nd} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		methaus.1	$⊢ J = MetOpen (D)$
2	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
3	2	adantr	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to J \in Top$
4		simpll	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to D \in ∞Met (X)$
5		simplr1	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to A \subseteq X$
6		simprr	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to y \in A$
7	5 6	sseldd	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to y \in X$
8		simprl	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to x \in ℕ$
9	8	nnrpd	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to x \in ℝ^{+}$
10	9	rpreccld	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to \frac{1}{x} \in ℝ^{+}$
11	10	rpxrd	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to \frac{1}{x} \in ℝ^{*}$
12	1	blopn	$⊢ (D \in ∞Met (X) \land y \in X \land \frac{1}{x} \in ℝ^{*}) \to y ball (D) (\frac{1}{x}) \in J$
13	4 7 11 12	syl3anc	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (x \in ℕ \land y \in A)) \to y ball (D) (\frac{1}{x}) \in J$
14	13	ralrimivva	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to \forall x \in ℕ \forall y \in A y ball (D) (\frac{1}{x}) \in J$
15		eqid	$⊢ (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) = (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))$
16	15	fmpo	$⊢ \forall x \in ℕ \forall y \in A y ball (D) (\frac{1}{x}) \in J \leftrightarrow (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) : ℕ \times A ⟶ J$
17	14 16	sylib	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) : ℕ \times A ⟶ J$
18	17	frnd	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \subseteq J$
19		simpll	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \to D \in ∞Met (X)$
20		simprl	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \to u \in J$
21		simprr	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \to z \in u$
22	1	mopni2	$⊢ (D \in ∞Met (X) \land u \in J \land z \in u) \to \exists r \in ℝ^{+} z ball (D) r \subseteq u$
23	19 20 21 22	syl3anc	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \to \exists r \in ℝ^{+} z ball (D) r \subseteq u$
24		simprl	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land (r \in ℝ^{+} \land z ball (D) r \subseteq u)) \to r \in ℝ^{+}$
25	24	rphalfcld	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land (r \in ℝ^{+} \land z ball (D) r \subseteq u)) \to \frac{r}{2} \in ℝ^{+}$
26		elrp	$⊢ \frac{r}{2} \in ℝ^{+} \leftrightarrow (\frac{r}{2} \in ℝ \land 0 < \frac{r}{2})$
27		nnrecl	$⊢ (\frac{r}{2} \in ℝ \land 0 < \frac{r}{2}) \to \exists n \in ℕ \frac{1}{n} < \frac{r}{2}$
28	26 27	sylbi	$⊢ \frac{r}{2} \in ℝ^{+} \to \exists n \in ℕ \frac{1}{n} < \frac{r}{2}$
29	25 28	syl	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land (r \in ℝ^{+} \land z ball (D) r \subseteq u)) \to \exists n \in ℕ \frac{1}{n} < \frac{r}{2}$
30	3	ad2antrr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to J \in Top$
31		simpr1	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to A \subseteq X$
32	31	ad2antrr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to A \subseteq X$
33	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
34	33	ad3antrrr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to X = ⋃ J$
35	32 34	sseqtrd	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to A \subseteq ⋃ J$
36		simplrr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z \in u$
37		simplrl	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to u \in J$
38		elunii	$⊢ (z \in u \land u \in J) \to z \in ⋃ J$
39	36 37 38	syl2anc	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z \in ⋃ J$
40	39 34	eleqtrrd	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z \in X$
41		simpr3	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to cls (J) (A) = X$
42	41	ad2antrr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to cls (J) (A) = X$
43	40 42	eleqtrrd	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z \in cls (J) (A)$
44	19	adantr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to D \in ∞Met (X)$
45		simprrl	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to n \in ℕ$
46	45	nnrpd	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to n \in ℝ^{+}$
47	46	rpreccld	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \frac{1}{n} \in ℝ^{+}$
48	47	rpxrd	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \frac{1}{n} \in ℝ^{*}$
49	1	blopn	$⊢ (D \in ∞Met (X) \land z \in X \land \frac{1}{n} \in ℝ^{*}) \to z ball (D) (\frac{1}{n}) \in J$
50	44 40 48 49	syl3anc	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z ball (D) (\frac{1}{n}) \in J$
51		blcntr	$⊢ (D \in ∞Met (X) \land z \in X \land \frac{1}{n} \in ℝ^{+}) \to z \in (z ball (D) (\frac{1}{n}))$
52	44 40 47 51	syl3anc	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z \in (z ball (D) (\frac{1}{n}))$
53		eqid	$⊢ ⋃ J = ⋃ J$
54	53	clsndisj	$⊢ ((J \in Top \land A \subseteq ⋃ J \land z \in cls (J) (A)) \land (z ball (D) (\frac{1}{n}) \in J \land z \in (z ball (D) (\frac{1}{n})))) \to (z ball (D) (\frac{1}{n})) \cap A \neq \emptyset$
55	30 35 43 50 52 54	syl32anc	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to (z ball (D) (\frac{1}{n})) \cap A \neq \emptyset$
56		n0	$⊢ (z ball (D) (\frac{1}{n})) \cap A \neq \emptyset \leftrightarrow \exists t t \in ((z ball (D) (\frac{1}{n})) \cap A)$
57	55 56	sylib	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \exists t t \in ((z ball (D) (\frac{1}{n})) \cap A)$
58	45	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to n \in ℕ$
59		simpr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t \in ((z ball (D) (\frac{1}{n})) \cap A)$
60	59	elin2d	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t \in A$
61		eqidd	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t ball (D) (\frac{1}{n}) = t ball (D) (\frac{1}{n})$
62		oveq2	$⊢ x = n \to \frac{1}{x} = \frac{1}{n}$
63	62	oveq2d	$⊢ x = n \to y ball (D) (\frac{1}{x}) = y ball (D) (\frac{1}{n})$
64	63	eqeq2d	$⊢ x = n \to (t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{x}) \leftrightarrow t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{n}))$
65		oveq1	$⊢ y = t \to y ball (D) (\frac{1}{n}) = t ball (D) (\frac{1}{n})$
66	65	eqeq2d	$⊢ y = t \to (t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{n}) \leftrightarrow t ball (D) (\frac{1}{n}) = t ball (D) (\frac{1}{n}))$
67	64 66	rspc2ev	$⊢ (n \in ℕ \land t \in A \land t ball (D) (\frac{1}{n}) = t ball (D) (\frac{1}{n})) \to \exists x \in ℕ \exists y \in A t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{x})$
68	58 60 61 67	syl3anc	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to \exists x \in ℕ \exists y \in A t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{x})$
69		ovex	$⊢ t ball (D) (\frac{1}{n}) \in V$
70		eqeq1	$⊢ z = t ball (D) (\frac{1}{n}) \to (z = y ball (D) (\frac{1}{x}) \leftrightarrow t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{x}))$
71	70	2rexbidv	$⊢ z = t ball (D) (\frac{1}{n}) \to (\exists x \in ℕ \exists y \in A z = y ball (D) (\frac{1}{x}) \leftrightarrow \exists x \in ℕ \exists y \in A t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{x}))$
72	15	rnmpo	$⊢ ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) = \{z \| \exists x \in ℕ \exists y \in A z = y ball (D) (\frac{1}{x})\}$
73	69 71 72	elab2	$⊢ t ball (D) (\frac{1}{n}) \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \leftrightarrow \exists x \in ℕ \exists y \in A t ball (D) (\frac{1}{n}) = y ball (D) (\frac{1}{x})$
74	68 73	sylibr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t ball (D) (\frac{1}{n}) \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))$
75	59	elin1d	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t \in (z ball (D) (\frac{1}{n}))$
76	44	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to D \in ∞Met (X)$
77	48	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to \frac{1}{n} \in ℝ^{*}$
78	40	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to z \in X$
79	32	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to A \subseteq X$
80	79 60	sseldd	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t \in X$
81		blcom	$⊢ ((D \in ∞Met (X) \land \frac{1}{n} \in ℝ^{*}) \land (z \in X \land t \in X)) \to (t \in (z ball (D) (\frac{1}{n})) \leftrightarrow z \in (t ball (D) (\frac{1}{n})))$
82	76 77 78 80 81	syl22anc	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to (t \in (z ball (D) (\frac{1}{n})) \leftrightarrow z \in (t ball (D) (\frac{1}{n})))$
83	75 82	mpbid	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to z \in (t ball (D) (\frac{1}{n}))$
84		simprll	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to r \in ℝ^{+}$
85	84	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to r \in ℝ^{+}$
86	85	rphalfcld	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to \frac{r}{2} \in ℝ^{+}$
87	86	rpxrd	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to \frac{r}{2} \in ℝ^{*}$
88		simprrr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \frac{1}{n} < \frac{r}{2}$
89	84	rphalfcld	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \frac{r}{2} \in ℝ^{+}$
90		rpre	$⊢ \frac{1}{n} \in ℝ^{+} \to \frac{1}{n} \in ℝ$
91		rpre	$⊢ \frac{r}{2} \in ℝ^{+} \to \frac{r}{2} \in ℝ$
92		ltle	$⊢ (\frac{1}{n} \in ℝ \land \frac{r}{2} \in ℝ) \to (\frac{1}{n} < \frac{r}{2} \to \frac{1}{n} \leq \frac{r}{2})$
93	90 91 92	syl2an	$⊢ (\frac{1}{n} \in ℝ^{+} \land \frac{r}{2} \in ℝ^{+}) \to (\frac{1}{n} < \frac{r}{2} \to \frac{1}{n} \leq \frac{r}{2})$
94	47 89 93	syl2anc	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to (\frac{1}{n} < \frac{r}{2} \to \frac{1}{n} \leq \frac{r}{2})$
95	88 94	mpd	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \frac{1}{n} \leq \frac{r}{2}$
96	95	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to \frac{1}{n} \leq \frac{r}{2}$
97		ssbl	$⊢ ((D \in ∞Met (X) \land t \in X) \land (\frac{1}{n} \in ℝ^{} \land \frac{r}{2} \in ℝ^{}) \land \frac{1}{n} \leq \frac{r}{2}) \to t ball (D) (\frac{1}{n}) \subseteq t ball (D) (\frac{r}{2})$
98	76 80 77 87 96 97	syl221anc	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t ball (D) (\frac{1}{n}) \subseteq t ball (D) (\frac{r}{2})$
99	85	rpred	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to r \in ℝ$
100	98 83	sseldd	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to z \in (t ball (D) (\frac{r}{2}))$
101		blhalf	$⊢ ((D \in ∞Met (X) \land t \in X) \land (r \in ℝ \land z \in (t ball (D) (\frac{r}{2})))) \to t ball (D) (\frac{r}{2}) \subseteq z ball (D) r$
102	76 80 99 100 101	syl22anc	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t ball (D) (\frac{r}{2}) \subseteq z ball (D) r$
103		simprlr	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to z ball (D) r \subseteq u$
104	103	adantr	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to z ball (D) r \subseteq u$
105	102 104	sstrd	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t ball (D) (\frac{r}{2}) \subseteq u$
106	98 105	sstrd	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to t ball (D) (\frac{1}{n}) \subseteq u$
107		eleq2	$⊢ w = t ball (D) (\frac{1}{n}) \to (z \in w \leftrightarrow z \in (t ball (D) (\frac{1}{n})))$
108		sseq1	$⊢ w = t ball (D) (\frac{1}{n}) \to (w \subseteq u \leftrightarrow t ball (D) (\frac{1}{n}) \subseteq u)$
109	107 108	anbi12d	$⊢ w = t ball (D) (\frac{1}{n}) \to ((z \in w \land w \subseteq u) \leftrightarrow (z \in (t ball (D) (\frac{1}{n})) \land t ball (D) (\frac{1}{n}) \subseteq u))$
110	109	rspcev	$⊢ (t ball (D) (\frac{1}{n}) \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \land (z \in (t ball (D) (\frac{1}{n})) \land t ball (D) (\frac{1}{n}) \subseteq u)) \to \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
111	74 83 106 110	syl12anc	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \land t \in ((z ball (D) (\frac{1}{n})) \cap A)) \to \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
112	57 111	exlimddv	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land ((r \in ℝ^{+} \land z ball (D) r \subseteq u) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2}))) \to \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
113	112	anassrs	$⊢ ((((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land (r \in ℝ^{+} \land z ball (D) r \subseteq u)) \land (n \in ℕ \land \frac{1}{n} < \frac{r}{2})) \to \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
114	29 113	rexlimddv	$⊢ (((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \land (r \in ℝ^{+} \land z ball (D) r \subseteq u)) \to \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
115	23 114	rexlimddv	$⊢ ((D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \land (u \in J \land z \in u)) \to \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
116	115	ralrimivva	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to \forall u \in J \forall z \in u \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)$
117		basgen2	$⊢ (J \in Top \land ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \subseteq J \land \forall u \in J \forall z \in u \exists w \in ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) (z \in w \land w \subseteq u)) \to topGen (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))) = J$
118	3 18 116 117	syl3anc	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to topGen (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))) = J$
119	118 3	eqeltrd	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to topGen (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))) \in Top$
120		tgclb	$⊢ ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \in TopBases \leftrightarrow topGen (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))) \in Top$
121	119 120	sylibr	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \in TopBases$
122		omelon	$⊢ ω \in On$
123		simpr2	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to A ≼ ω$
124		nnex	$⊢ ℕ \in V$
125	124	xpdom2	$⊢ A ≼ ω \to (ℕ \times A) ≼ (ℕ \times ω)$
126	123 125	syl	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to (ℕ \times A) ≼ (ℕ \times ω)$
127		nnenom	$⊢ ℕ \approx ω$
128		omex	$⊢ ω \in V$
129	128	enref	$⊢ ω \approx ω$
130		xpen	$⊢ (ℕ \approx ω \land ω \approx ω) \to (ℕ \times ω) \approx (ω \times ω)$
131	127 129 130	mp2an	$⊢ (ℕ \times ω) \approx (ω \times ω)$
132		xpomen	$⊢ (ω \times ω) \approx ω$
133	131 132	entri	$⊢ (ℕ \times ω) \approx ω$
134		domentr	$⊢ ((ℕ \times A) ≼ (ℕ \times ω) \land (ℕ \times ω) \approx ω) \to (ℕ \times A) ≼ ω$
135	126 133 134	sylancl	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to (ℕ \times A) ≼ ω$
136		ondomen	$⊢ (ω \in On \land (ℕ \times A) ≼ ω) \to ℕ \times A \in dom card$
137	122 135 136	sylancr	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to ℕ \times A \in dom card$
138	17	ffnd	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) Fn (ℕ \times A)$
139		dffn4	$⊢ (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) Fn (ℕ \times A) \leftrightarrow (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) : ℕ \times A \underset{onto}{⟶} ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))$
140	138 139	sylib	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) : ℕ \times A \underset{onto}{⟶} ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))$
141		fodomnum	$⊢ ℕ \times A \in dom card \to ((x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) : ℕ \times A \underset{onto}{⟶} ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \to ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) ≼ (ℕ \times A))$
142	137 140 141	sylc	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) ≼ (ℕ \times A)$
143		domtr	$⊢ (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) ≼ (ℕ \times A) \land (ℕ \times A) ≼ ω) \to ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) ≼ ω$
144	142 135 143	syl2anc	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) ≼ ω$
145		2ndci	$⊢ (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) \in TopBases \land ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x})) ≼ ω) \to topGen (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))) \in 2^{nd} 𝜔$
146	121 144 145	syl2anc	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to topGen (ran (x \in ℕ, y \in A ⟼ y ball (D) (\frac{1}{x}))) \in 2^{nd} 𝜔$
147	118 146	eqeltrrd	$⊢ (D \in ∞Met (X) \land (A \subseteq X \land A ≼ ω \land cls (J) (A) = X)) \to J \in 2^{nd} 𝜔$

Metamath Proof Explorer

Theorem met2ndci

Proof