metcld2

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 Mario Carneiro, 1-May-2014)

		Ref	Expression
	Hypothesis	metcld.2	$⊢ J = MetOpen (D)$
	Assertion	metcld2	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow \underset{t}{⇝} (J) [S^{ℕ}] \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		metcld.2	$⊢ J = MetOpen (D)$
2	1	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))$
3		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)$
4		vex	$⊢ x \in V$
5	4	elima2	$⊢ x \in \underset{t}{⇝} (J) [S^{ℕ}] \leftrightarrow \exists f (f \in (S^{ℕ}) \land f \underset{t}{⇝} (J) x)$
6		id	$⊢ S \subseteq X \to S \subseteq X$
7		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
8		ssexg	$⊢ (S \subseteq X \land X \in dom ∞Met) \to S \in V$
9	6 7 8	syl2anr	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to S \in V$
10		nnex	$⊢ ℕ \in V$
11		elmapg	$⊢ (S \in V \land ℕ \in V) \to (f \in (S^{ℕ}) \leftrightarrow f : ℕ ⟶ S)$
12	9 10 11	sylancl	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (f \in (S^{ℕ}) \leftrightarrow f : ℕ ⟶ S)$
13	12	anbi1d	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to ((f \in (S^{ℕ}) \land f \underset{t}{⇝} (J) x) \leftrightarrow (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x))$
14	13	exbidv	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (\exists f (f \in (S^{ℕ}) \land f \underset{t}{⇝} (J) x) \leftrightarrow \exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x))$
15	5 14	bitr2id	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (\exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \leftrightarrow x \in \underset{t}{⇝} (J) [S^{ℕ}])$
16	15	imbi1d	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to ((\exists f (f : ℕ ⟶ S \land f \underset{t}{⇝} (J) x) \to x \in S) \leftrightarrow (x \in \underset{t}{⇝} (J) [S^{ℕ}] \to x \in S))$
17	3 16	syl5bb	$⊢ (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 \underset{t}{⇝} (J) [S^{ℕ}] \to x \in S))$
18	17	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 \underset{t}{⇝} (J) [S^{ℕ}] \to x \in S))$
19		dfss2	$⊢ \underset{t}{⇝} (J) [S^{ℕ}] \subseteq S \leftrightarrow \forall x (x \in \underset{t}{⇝} (J) [S^{ℕ}] \to x \in S)$
20	18 19	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 \underset{t}{⇝} (J) [S^{ℕ}] \subseteq S)$
21	2 20	bitrd	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow \underset{t}{⇝} (J) [S^{ℕ}] \subseteq S)$

Metamath Proof Explorer

Theorem metcld2

Proof