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	syl5bi	⊢ ( ( ( 𝐽 ∈ 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 𝐹 ) )