lmmo

Description: A sequence in a Hausdorff space converges to at most one limit. Part of Lemma 1.4-2(a) of Kreyszig p. 26. (Contributed by NM, 31-Jan-2008) (Proof shortened by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmmo.1	$⊢ φ \to J \in Haus$
	lmmo.4	$⊢ φ \to F \underset{t}{⇝} (J) A$
	lmmo.5	$⊢ φ \to F \underset{t}{⇝} (J) B$
Assertion	lmmo	$⊢ φ \to A = B$

Proof

Step	Hyp	Ref	Expression
1		lmmo.1	$⊢ φ \to J \in Haus$
2		lmmo.4	$⊢ φ \to F \underset{t}{⇝} (J) A$
3		lmmo.5	$⊢ φ \to F \underset{t}{⇝} (J) B$
4		an4	$⊢ ((x \in J \land y \in J) \land (A \in x \land B \in y)) \leftrightarrow ((x \in J \land A \in x) \land (y \in J \land B \in y))$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		simprr	$⊢ (φ \land (x \in J \land A \in x)) \to A \in x$
7		1zzd	$⊢ (φ \land (x \in J \land A \in x)) \to 1 \in ℤ$
8	2	adantr	$⊢ (φ \land (x \in J \land A \in x)) \to F \underset{t}{⇝} (J) A$
9		simprl	$⊢ (φ \land (x \in J \land A \in x)) \to x \in J$
10	5 6 7 8 9	lmcvg	$⊢ (φ \land (x \in J \land A \in x)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in x$
11	10	ex	$⊢ φ \to ((x \in J \land A \in x) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in x)$
12		simprr	$⊢ (φ \land (y \in J \land B \in y)) \to B \in y$
13		1zzd	$⊢ (φ \land (y \in J \land B \in y)) \to 1 \in ℤ$
14	3	adantr	$⊢ (φ \land (y \in J \land B \in y)) \to F \underset{t}{⇝} (J) B$
15		simprl	$⊢ (φ \land (y \in J \land B \in y)) \to y \in J$
16	5 12 13 14 15	lmcvg	$⊢ (φ \land (y \in J \land B \in y)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in y$
17	16	ex	$⊢ φ \to ((y \in J \land B \in y) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in y)$
18	11 17	anim12d	$⊢ φ \to (((x \in J \land A \in x) \land (y \in J \land B \in y)) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in x \land \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in y))$
19	5	rexanuz2	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y) \leftrightarrow (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in x \land \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in y)$
20		nnz	$⊢ j \in ℕ \to j \in ℤ$
21		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
22		ne0i	$⊢ j \in ℤ_{\geq j} \to ℤ_{\geq j} \neq \emptyset$
23	20 21 22	3syl	$⊢ j \in ℕ \to ℤ_{\geq j} \neq \emptyset$
24		r19.2z	$⊢ (ℤ_{\geq j} \neq \emptyset \land \forall k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y)) \to \exists k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y)$
25		elin	$⊢ F (k) \in (x \cap y) \leftrightarrow (F (k) \in x \land F (k) \in y)$
26		n0i	$⊢ F (k) \in (x \cap y) \to \neg x \cap y = \emptyset$
27	25 26	sylbir	$⊢ (F (k) \in x \land F (k) \in y) \to \neg x \cap y = \emptyset$
28	27	rexlimivw	$⊢ \exists k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y) \to \neg x \cap y = \emptyset$
29	24 28	syl	$⊢ (ℤ_{\geq j} \neq \emptyset \land \forall k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y)) \to \neg x \cap y = \emptyset$
30	23 29	sylan	$⊢ (j \in ℕ \land \forall k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y)) \to \neg x \cap y = \emptyset$
31	30	rexlimiva	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} (F (k) \in x \land F (k) \in y) \to \neg x \cap y = \emptyset$
32	19 31	sylbir	$⊢ (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in x \land \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) \in y) \to \neg x \cap y = \emptyset$
33	18 32	syl6	$⊢ φ \to (((x \in J \land A \in x) \land (y \in J \land B \in y)) \to \neg x \cap y = \emptyset)$
34	4 33	biimtrid	$⊢ φ \to (((x \in J \land y \in J) \land (A \in x \land B \in y)) \to \neg x \cap y = \emptyset)$
35	34	expdimp	$⊢ (φ \land (x \in J \land y \in J)) \to ((A \in x \land B \in y) \to \neg x \cap y = \emptyset)$
36		imnan	$⊢ ((A \in x \land B \in y) \to \neg x \cap y = \emptyset) \leftrightarrow \neg ((A \in x \land B \in y) \land x \cap y = \emptyset)$
37	35 36	sylib	$⊢ (φ \land (x \in J \land y \in J)) \to \neg ((A \in x \land B \in y) \land x \cap y = \emptyset)$
38		df-3an	$⊢ (A \in x \land B \in y \land x \cap y = \emptyset) \leftrightarrow ((A \in x \land B \in y) \land x \cap y = \emptyset)$
39	37 38	sylnibr	$⊢ (φ \land (x \in J \land y \in J)) \to \neg (A \in x \land B \in y \land x \cap y = \emptyset)$
40	39	anassrs	$⊢ ((φ \land x \in J) \land y \in J) \to \neg (A \in x \land B \in y \land x \cap y = \emptyset)$
41	40	nrexdv	$⊢ (φ \land x \in J) \to \neg \exists y \in J (A \in x \land B \in y \land x \cap y = \emptyset)$
42	41	nrexdv	$⊢ φ \to \neg \exists x \in J \exists y \in J (A \in x \land B \in y \land x \cap y = \emptyset)$
43		haustop	$⊢ J \in Haus \to J \in Top$
44	1 43	syl	$⊢ φ \to J \in Top$
45		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
46	44 45	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
47		lmcl	$⊢ (J \in TopOn (⋃ J) \land F \underset{t}{⇝} (J) A) \to A \in ⋃ J$
48	46 2 47	syl2anc	$⊢ φ \to A \in ⋃ J$
49		lmcl	$⊢ (J \in TopOn (⋃ J) \land F \underset{t}{⇝} (J) B) \to B \in ⋃ J$
50	46 3 49	syl2anc	$⊢ φ \to B \in ⋃ J$
51		eqid	$⊢ ⋃ J = ⋃ J$
52	51	hausnei	$⊢ (J \in Haus \land (A \in ⋃ J \land B \in ⋃ J \land A \neq B)) \to \exists x \in J \exists y \in J (A \in x \land B \in y \land x \cap y = \emptyset)$
53	52	3exp2	$⊢ J \in Haus \to (A \in ⋃ J \to (B \in ⋃ J \to (A \neq B \to \exists x \in J \exists y \in J (A \in x \land B \in y \land x \cap y = \emptyset))))$
54	1 48 50 53	syl3c	$⊢ φ \to (A \neq B \to \exists x \in J \exists y \in J (A \in x \land B \in y \land x \cap y = \emptyset))$
55	54	necon1bd	$⊢ φ \to (\neg \exists x \in J \exists y \in J (A \in x \land B \in y \land x \cap y = \emptyset) \to A = B)$
56	42 55	mpd	$⊢ φ \to A = B$

Metamath Proof Explorer

Theorem lmmo

Proof