Metamath Proof Explorer

Theorem metcld

Description: A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of Kreyszig p. 30. (Contributed by NM, 11-Nov-2007) (Revised by Mario Carneiro, 1-May-2014)

		Ref	Expression
	Hypothesis	metcld.2	$⊢ J = MetOpen (D)$
	Assertion	metcld	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow \forall x \forall f ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S))$

Proof

Step	Hyp	Ref	Expression
1		metcld.2	$⊢ 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	sseq2d	$⊢ D \in ∞Met (X) \to (S \subseteq X \leftrightarrow S \subseteq ⋃ J)$
5	4	biimpa	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to S \subseteq ⋃ J$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	6	iscld4	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) \subseteq S)$
8	2 5 7	syl2an2r	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) \subseteq S)$
9		19.23v	$⊢ \forall f ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S) \leftrightarrow (\exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S)$
10		simpl	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to D \in ∞Met (X)$
11		simpr	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to S \subseteq X$
12	1 10 11	metelcls	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (x \in cls (J) (S) \leftrightarrow \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x))$
13	12	imbi1d	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to ((x \in cls (J) (S) \to x \in S) \leftrightarrow (\exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S))$
14	9 13	bitr4id	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (\forall f ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S) \leftrightarrow (x \in cls (J) (S) \to x \in S))$
15	14	albidv	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (\forall x \forall f ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S) \leftrightarrow \forall x (x \in cls (J) (S) \to x \in S))$
16		dfss2	$⊢ cls (J) (S) \subseteq S \leftrightarrow \forall x (x \in cls (J) (S) \to x \in S)$
17	15 16	bitr4di	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (\forall x \forall f ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S) \leftrightarrow cls (J) (S) \subseteq S)$
18	8 17	bitr4d	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow \forall x \forall f ((f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S))$