This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ) ) → ¬ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
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 ⊢ ( 𝜑 → 𝐴 = 𝐵 )