met1stc

Description: The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Hypothesis	methaus.1	$⊢ J = MetOpen (D)$
	Assertion	met1stc	$⊢ D \in ∞Met (X) \to J \in 1^{st} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		methaus.1	$⊢ J = MetOpen (D)$
2	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
3	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
4	3	eleq2d	$⊢ D \in ∞Met (X) \to (x \in X \leftrightarrow x \in ⋃ J)$
5	4	biimpar	$⊢ (D \in ∞Met (X) \land x \in ⋃ J) \to x \in X$
6		simpll	$⊢ ((D \in ∞Met (X) \land x \in X) \land n \in ℕ) \to D \in ∞Met (X)$
7		simplr	$⊢ ((D \in ∞Met (X) \land x \in X) \land n \in ℕ) \to x \in X$
8		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
9	8	adantl	$⊢ ((D \in ∞Met (X) \land x \in X) \land n \in ℕ) \to n \in ℝ^{+}$
10	9	rpreccld	$⊢ ((D \in ∞Met (X) \land x \in X) \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
11	10	rpxrd	$⊢ ((D \in ∞Met (X) \land x \in X) \land n \in ℕ) \to \frac{1}{n} \in ℝ^{*}$
12	1	blopn	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{1}{n} \in ℝ^{*}) \to x ball (D) (\frac{1}{n}) \in J$
13	6 7 11 12	syl3anc	$⊢ ((D \in ∞Met (X) \land x \in X) \land n \in ℕ) \to x ball (D) (\frac{1}{n}) \in J$
14	13	fmpttd	$⊢ (D \in ∞Met (X) \land x \in X) \to (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) : ℕ ⟶ J$
15	14	frnd	$⊢ (D \in ∞Met (X) \land x \in X) \to ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \subseteq J$
16		nnex	$⊢ ℕ \in V$
17	16	mptex	$⊢ (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \in V$
18	17	rnex	$⊢ ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \in V$
19	18	elpw	$⊢ ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \in 𝒫 J \leftrightarrow ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \subseteq J$
20	15 19	sylibr	$⊢ (D \in ∞Met (X) \land x \in X) \to ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \in 𝒫 J$
21		omelon	$⊢ ω \in On$
22		nnenom	$⊢ ℕ \approx ω$
23	22	ensymi	$⊢ ω \approx ℕ$
24		isnumi	$⊢ (ω \in On \land ω \approx ℕ) \to ℕ \in dom card$
25	21 23 24	mp2an	$⊢ ℕ \in dom card$
26		ovex	$⊢ x ball (D) (\frac{1}{n}) \in V$
27		eqid	$⊢ (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) = (n \in ℕ ⟼ x ball (D) (\frac{1}{n}))$
28	26 27	fnmpti	$⊢ (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) Fn ℕ$
29		dffn4	$⊢ (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) Fn ℕ \leftrightarrow (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) : ℕ \underset{onto}{⟶} ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n}))$
30	28 29	mpbi	$⊢ (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) : ℕ \underset{onto}{⟶} ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n}))$
31		fodomnum	$⊢ ℕ \in dom card \to ((n \in ℕ ⟼ x ball (D) (\frac{1}{n})) : ℕ \underset{onto}{⟶} ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \to ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ℕ)$
32	25 30 31	mp2	$⊢ ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ℕ$
33		domentr	$⊢ (ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ℕ \land ℕ \approx ω) \to ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ω$
34	32 22 33	mp2an	$⊢ ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ω$
35	34	a1i	$⊢ (D \in ∞Met (X) \land x \in X) \to ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ω$
36		simpll	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to D \in ∞Met (X)$
37		simprl	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to z \in J$
38		simprr	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to x \in z$
39	1	mopni2	$⊢ (D \in ∞Met (X) \land z \in J \land x \in z) \to \exists r \in ℝ^{+} x ball (D) r \subseteq z$
40	36 37 38 39	syl3anc	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to \exists r \in ℝ^{+} x ball (D) r \subseteq z$
41		simp-4l	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to D \in ∞Met (X)$
42		simp-4r	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to x \in X$
43		simprl	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to y \in ℕ$
44	43	nnrpd	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to y \in ℝ^{+}$
45	44	rpreccld	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to \frac{1}{y} \in ℝ^{+}$
46		blcntr	$⊢ (D \in ∞Met (X) \land x \in X \land \frac{1}{y} \in ℝ^{+}) \to x \in (x ball (D) (\frac{1}{y}))$
47	41 42 45 46	syl3anc	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to x \in (x ball (D) (\frac{1}{y}))$
48	45	rpxrd	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to \frac{1}{y} \in ℝ^{*}$
49		simplrl	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to r \in ℝ^{+}$
50	49	rpxrd	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to r \in ℝ^{*}$
51		nnrecre	$⊢ y \in ℕ \to \frac{1}{y} \in ℝ$
52	51	ad2antrl	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to \frac{1}{y} \in ℝ$
53	49	rpred	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to r \in ℝ$
54		simprr	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to \frac{1}{y} < r$
55	52 53 54	ltled	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to \frac{1}{y} \leq r$
56		ssbl	$⊢ ((D \in ∞Met (X) \land x \in X) \land (\frac{1}{y} \in ℝ^{} \land r \in ℝ^{}) \land \frac{1}{y} \leq r) \to x ball (D) (\frac{1}{y}) \subseteq x ball (D) r$
57	41 42 48 50 55 56	syl221anc	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to x ball (D) (\frac{1}{y}) \subseteq x ball (D) r$
58		simplrr	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to x ball (D) r \subseteq z$
59	57 58	sstrd	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to x ball (D) (\frac{1}{y}) \subseteq z$
60	47 59	jca	$⊢ ((((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \land (y \in ℕ \land \frac{1}{y} < r)) \to (x \in (x ball (D) (\frac{1}{y})) \land x ball (D) (\frac{1}{y}) \subseteq z)$
61		elrp	$⊢ r \in ℝ^{+} \leftrightarrow (r \in ℝ \land 0 < r)$
62		nnrecl	$⊢ (r \in ℝ \land 0 < r) \to \exists y \in ℕ \frac{1}{y} < r$
63	61 62	sylbi	$⊢ r \in ℝ^{+} \to \exists y \in ℕ \frac{1}{y} < r$
64	63	ad2antrl	$⊢ (((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \to \exists y \in ℕ \frac{1}{y} < r$
65	60 64	reximddv	$⊢ (((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land (r \in ℝ^{+} \land x ball (D) r \subseteq z)) \to \exists y \in ℕ (x \in (x ball (D) (\frac{1}{y})) \land x ball (D) (\frac{1}{y}) \subseteq z)$
66	40 65	rexlimddv	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to \exists y \in ℕ (x \in (x ball (D) (\frac{1}{y})) \land x ball (D) (\frac{1}{y}) \subseteq z)$
67		ovexd	$⊢ (((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land y \in ℕ) \to x ball (D) (\frac{1}{y}) \in V$
68		vex	$⊢ w \in V$
69		oveq2	$⊢ n = y \to \frac{1}{n} = \frac{1}{y}$
70	69	oveq2d	$⊢ n = y \to x ball (D) (\frac{1}{n}) = x ball (D) (\frac{1}{y})$
71	70	cbvmptv	$⊢ (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) = (y \in ℕ ⟼ x ball (D) (\frac{1}{y}))$
72	71	elrnmpt	$⊢ w \in V \to (w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \leftrightarrow \exists y \in ℕ w = x ball (D) (\frac{1}{y}))$
73	68 72	mp1i	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to (w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \leftrightarrow \exists y \in ℕ w = x ball (D) (\frac{1}{y}))$
74		eleq2	$⊢ w = x ball (D) (\frac{1}{y}) \to (x \in w \leftrightarrow x \in (x ball (D) (\frac{1}{y})))$
75		sseq1	$⊢ w = x ball (D) (\frac{1}{y}) \to (w \subseteq z \leftrightarrow x ball (D) (\frac{1}{y}) \subseteq z)$
76	74 75	anbi12d	$⊢ w = x ball (D) (\frac{1}{y}) \to ((x \in w \land w \subseteq z) \leftrightarrow (x \in (x ball (D) (\frac{1}{y})) \land x ball (D) (\frac{1}{y}) \subseteq z))$
77	76	adantl	$⊢ (((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \land w = x ball (D) (\frac{1}{y})) \to ((x \in w \land w \subseteq z) \leftrightarrow (x \in (x ball (D) (\frac{1}{y})) \land x ball (D) (\frac{1}{y}) \subseteq z))$
78	67 73 77	rexxfr2d	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to (\exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z) \leftrightarrow \exists y \in ℕ (x \in (x ball (D) (\frac{1}{y})) \land x ball (D) (\frac{1}{y}) \subseteq z))$
79	66 78	mpbird	$⊢ ((D \in ∞Met (X) \land x \in X) \land (z \in J \land x \in z)) \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z)$
80	79	expr	$⊢ ((D \in ∞Met (X) \land x \in X) \land z \in J) \to (x \in z \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z))$
81	80	ralrimiva	$⊢ (D \in ∞Met (X) \land x \in X) \to \forall z \in J (x \in z \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z))$
82		breq1	$⊢ y = ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \to (y ≼ ω \leftrightarrow ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ω)$
83		rexeq	$⊢ y = ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \to (\exists w \in y (x \in w \land w \subseteq z) \leftrightarrow \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z))$
84	83	imbi2d	$⊢ y = ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \to ((x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow (x \in z \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z)))$
85	84	ralbidv	$⊢ y = ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \to (\forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z)) \leftrightarrow \forall z \in J (x \in z \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z)))$
86	82 85	anbi12d	$⊢ y = ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \to ((y ≼ ω \land \forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z))) \leftrightarrow (ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ω \land \forall z \in J (x \in z \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z))))$
87	86	rspcev	$⊢ (ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) \in 𝒫 J \land (ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) ≼ ω \land \forall z \in J (x \in z \to \exists w \in ran (n \in ℕ ⟼ x ball (D) (\frac{1}{n})) (x \in w \land w \subseteq z)))) \to \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
88	20 35 81 87	syl12anc	$⊢ (D \in ∞Met (X) \land x \in X) \to \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
89	5 88	syldan	$⊢ (D \in ∞Met (X) \land x \in ⋃ J) \to \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
90	89	ralrimiva	$⊢ D \in ∞Met (X) \to \forall x \in ⋃ J \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z)))$
91		eqid	$⊢ ⋃ J = ⋃ J$
92	91	is1stc2	$⊢ J \in 1^{st} 𝜔 \leftrightarrow (J \in Top \land \forall x \in ⋃ J \exists y \in 𝒫 J (y ≼ ω \land \forall z \in J (x \in z \to \exists w \in y (x \in w \land w \subseteq z))))$
93	2 90 92	sylanbrc	$⊢ D \in ∞Met (X) \to J \in 1^{st} 𝜔$

Metamath Proof Explorer

Theorem met1stc

Proof