lmcls

Description: Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmff.1	$⊢ Z = ℤ_{\geq M}$
	lmff.3	$⊢ φ \to J \in TopOn (X)$
	lmff.4	$⊢ φ \to M \in ℤ$
	lmcls.5	$⊢ φ \to F \underset{t}{⇝} (J) P$
	lmcls.7	$⊢ (φ \land k \in Z) \to F (k) \in S$
	lmcls.8	$⊢ φ \to S \subseteq X$
Assertion	lmcls	$⊢ φ \to P \in cls (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		lmff.1	$⊢ Z = ℤ_{\geq M}$
2		lmff.3	$⊢ φ \to J \in TopOn (X)$
3		lmff.4	$⊢ φ \to M \in ℤ$
4		lmcls.5	$⊢ φ \to F \underset{t}{⇝} (J) P$
5		lmcls.7	$⊢ (φ \land k \in Z) \to F (k) \in S$
6		lmcls.8	$⊢ φ \to S \subseteq X$
7	2 1 3	lmbr2	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
8	4 7	mpbid	$⊢ φ \to (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
9	8	simp3d	$⊢ φ \to \forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
10	1	r19.2uz	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \to \exists k \in Z (k \in dom F \land F (k) \in u)$
11		inelcm	$⊢ (F (k) \in u \land F (k) \in S) \to u \cap S \neq \emptyset$
12	11	a1i	$⊢ (φ \land k \in Z) \to ((F (k) \in u \land F (k) \in S) \to u \cap S \neq \emptyset)$
13	5 12	mpan2d	$⊢ (φ \land k \in Z) \to (F (k) \in u \to u \cap S \neq \emptyset)$
14	13	adantld	$⊢ (φ \land k \in Z) \to ((k \in dom F \land F (k) \in u) \to u \cap S \neq \emptyset)$
15	14	rexlimdva	$⊢ φ \to (\exists k \in Z (k \in dom F \land F (k) \in u) \to u \cap S \neq \emptyset)$
16	10 15	syl5	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \to u \cap S \neq \emptyset)$
17	16	imim2d	$⊢ φ \to ((P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \to (P \in u \to u \cap S \neq \emptyset))$
18	17	ralimdv	$⊢ φ \to (\forall u \in J (P \in u \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)) \to \forall u \in J (P \in u \to u \cap S \neq \emptyset))$
19	9 18	mpd	$⊢ φ \to \forall u \in J (P \in u \to u \cap S \neq \emptyset)$
20		topontop	$⊢ J \in TopOn (X) \to J \in Top$
21	2 20	syl	$⊢ φ \to J \in Top$
22		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
23	2 22	syl	$⊢ φ \to X = ⋃ J$
24	6 23	sseqtrd	$⊢ φ \to S \subseteq ⋃ J$
25		lmcl	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to P \in X$
26	2 4 25	syl2anc	$⊢ φ \to P \in X$
27	26 23	eleqtrd	$⊢ φ \to P \in ⋃ J$
28		eqid	$⊢ ⋃ J = ⋃ J$
29	28	elcls	$⊢ (J \in Top \land S \subseteq ⋃ J \land P \in ⋃ J) \to (P \in cls (J) (S) \leftrightarrow \forall u \in J (P \in u \to u \cap S \neq \emptyset))$
30	21 24 27 29	syl3anc	$⊢ φ \to (P \in cls (J) (S) \leftrightarrow \forall u \in J (P \in u \to u \cap S \neq \emptyset))$
31	19 30	mpbird	$⊢ φ \to P \in cls (J) (S)$

Metamath Proof Explorer

Theorem lmcls

Proof