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

Metamath Proof Explorer

Theorem hausflimi

Description: One direction of hausflim . A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010) (Revised by Mario Carneiro, 21-Sep-2015)

Ref Expression
Assertion hausflimi ( 𝐽 ∈ Haus → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐽 ∈ Haus )
2 simprll ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 flimelbas ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) → 𝑥 ∈ ∪ 𝐽 )
5 2 4 syl ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ∪ 𝐽 )
6 simprlr ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ ( 𝐽 fLim 𝐹 ) )
7 3 flimelbas ⊢ ( 𝑦 ∈ ( 𝐽 fLim 𝐹 ) → 𝑦 ∈ ∪ 𝐽 )
8 6 7 syl ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ ∪ 𝐽 )
9 simprr ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
10 3 hausnei ⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
11 1 5 8 9 10 syl13anc ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
12 df-3an ⊢ ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) ↔ ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) )
13 simprl ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) )
14 hausflimlem ⊢ ( ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ≠ ∅ )
15 14 3expa ⊢ ( ( ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ≠ ∅ )
16 13 15 sylanl1 ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ≠ ∅ )
17 16 a1d ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑢 ∩ 𝑣 ) ≠ ∅ ) )
18 17 necon4d ⊢ ( ( ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ) → ( ( 𝑢 ∩ 𝑣 ) = ∅ → 𝑥 = 𝑦 ) )
19 18 expimpd ⊢ ( ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) → ( ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ) ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑥 = 𝑦 ) )
20 12 19 biimtrid ⊢ ( ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ ( 𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) ) → ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑥 = 𝑦 ) )
21 20 rexlimdvva ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ ( 𝑢 ∩ 𝑣 ) = ∅ ) → 𝑥 = 𝑦 ) )
22 11 21 mpd ⊢ ( ( 𝐽 ∈ Haus ∧ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 = 𝑦 )
23 22 expr ⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ) → ( 𝑥 ≠ 𝑦 → 𝑥 = 𝑦 ) )
24 23 necon1bd ⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ) → ( ¬ 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
25 24 pm2.18d ⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) ) → 𝑥 = 𝑦 )
26 25 ex ⊢ ( 𝐽 ∈ Haus → ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 = 𝑦 ) )
27 26 alrimivv ⊢ ( 𝐽 ∈ Haus → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 = 𝑦 ) )
28 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) )
29 28 mo4 ⊢ ( ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 fLim 𝐹 ) ) → 𝑥 = 𝑦 ) )
30 27 29 sylibr ⊢ ( 𝐽 ∈ Haus → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )