Theorem 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	⊢ ( 𝜑 → 𝐽 ∈ Haus )
	lmmo.4	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐴 )
	lmmo.5	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐵 )
Assertion	lmmo	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lmmo.1	⊢ ( 𝜑 → 𝐽 ∈ Haus )
2		lmmo.4	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐴 )
3		lmmo.5	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐵 )
4		an4	⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) )
5		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
6		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → 𝐴 ∈ 𝑥 )
7		1zzd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → 1 ∈ ℤ )
8	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐴 )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → 𝑥 ∈ 𝐽 )
10	5 6 7 8 9	lmcvg	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 )
11	10	ex	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) )
12		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → 𝐵 ∈ 𝑦 )
13		1zzd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → 1 ∈ ℤ )
14	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐵 )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐽 )
16	5 12 13 14 15	lmcvg	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 )
17	16	ex	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) )
18	11 17	anim12d	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) ) )
19	5	rexanuz2	⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) ↔ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) )
20		nnz	⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
21		uzid	⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
22		ne0i	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ℤ≥ ‘ 𝑗 ) ≠ ∅ )
23	20 21 22	3syl	⊢ ( 𝑗 ∈ ℕ → ( ℤ≥ ‘ 𝑗 ) ≠ ∅ )
24		r19.2z	⊢ ( ( ( ℤ≥ ‘ 𝑗 ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) )
25		elin	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) )
26		n0i	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 ∩ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
27	25 26	sylbir	⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
28	27	rexlimivw	⊢ ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
29	24 28	syl	⊢ ( ( ( ℤ≥ ‘ 𝑗 ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
30	23 29	sylan	⊢ ( ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
31	30	rexlimiva	⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
32	19 31	sylbir	⊢ ( ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ )
33	18 32	syl6	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦 ) ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
34	4 33	syl5bi	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
35	34	expdimp	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
36		imnan	⊢ ( ( ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ¬ ( ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
37	35 36	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ¬ ( ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
38		df-3an	⊢ ( ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
39	37 38	sylnibr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ¬ ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
40	39	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) → ¬ ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
41	40	nrexdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ¬ ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
42	41	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
43		haustop	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
44	1 43	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
45		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
46	44 45	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
47		lmcl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐴 ) → 𝐴 ∈ ∪ 𝐽 )
48	46 2 47	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝐽 )
49		lmcl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝐵 ) → 𝐵 ∈ ∪ 𝐽 )
50	46 3 49	syl2anc	⊢ ( 𝜑 → 𝐵 ∈ ∪ 𝐽 )
51		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
52	51	hausnei	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝐴 ∈ ∪ 𝐽 ∧ 𝐵 ∈ ∪ 𝐽 ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
53	52	3exp2	⊢ ( 𝐽 ∈ Haus → ( 𝐴 ∈ ∪ 𝐽 → ( 𝐵 ∈ ∪ 𝐽 → ( 𝐴 ≠ 𝐵 → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) )
54	1 48 50 53	syl3c	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
55	54	necon1bd	⊢ ( 𝜑 → ( ¬ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝐴 = 𝐵 ) )
56	42 55	mpd	⊢ ( 𝜑 → 𝐴 = 𝐵 )