Theorem hausflimi 23867

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

Assertion

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

Distinct variable groups:   𝑥,𝐹   𝑥,𝐽

Proof of Theorem hausflimi

Dummy variables 𝑣 𝑢 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 482	. . . . . . . . 9 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝐽 ∈ Haus)
2		simprll 778	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ (𝐽 fLim 𝐹))
3		eqid 2729	. . . . . . . . . . 11 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	flimelbas 23855	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐽 fLim 𝐹) → 𝑥 ∈ ∪ 𝐽)
5	2, 4	syl 17	. . . . . . . . 9 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ ∪ 𝐽)
6		simprlr 779	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ (𝐽 fLim 𝐹))
7	3	flimelbas 23855	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐽 fLim 𝐹) → 𝑦 ∈ ∪ 𝐽)
8	6, 7	syl 17	. . . . . . . . 9 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ ∪ 𝐽)
9		simprr 772	. . . . . . . . 9 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝑥 ≠ 𝑦)
10	3	hausnei 23215	. . . . . . . . 9 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))
11	1, 5, 8, 9, 10	syl13anc 1374	. . . . . . . 8 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅))
12		df-3an 1088	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) ↔ ((𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣) ∧ (𝑢 ∩ 𝑣) = ∅))
13		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → (𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)))
14		hausflimlem 23866	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽) ∧ (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣)) → (𝑢 ∩ 𝑣) ≠ ∅)
15	14	3expa 1118	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣)) → (𝑢 ∩ 𝑣) ≠ ∅)
16	13, 15	sylanl1 680	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣)) → (𝑢 ∩ 𝑣) ≠ ∅)
17	16	a1d 25	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣)) → (𝑥 ≠ 𝑦 → (𝑢 ∩ 𝑣) ≠ ∅))
18	17	necon4d 2949	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) ∧ (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣)) → ((𝑢 ∩ 𝑣) = ∅ → 𝑥 = 𝑦))
19	18	expimpd 453	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) → (((𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣) ∧ (𝑢 ∩ 𝑣) = ∅) → 𝑥 = 𝑦))
20	12, 19	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) ∧ (𝑢 ∈ 𝐽 ∧ 𝑣 ∈ 𝐽)) → ((𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) → 𝑥 = 𝑦))
21	20	rexlimdvva 3194	. . . . . . . 8 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → (∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑣 ∧ (𝑢 ∩ 𝑣) = ∅) → 𝑥 = 𝑦))
22	11, 21	mpd 15	. . . . . . 7 ⊢ ((𝐽 ∈ Haus ∧ ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) ∧ 𝑥 ≠ 𝑦)) → 𝑥 = 𝑦)
23	22	expr 456	. . . . . 6 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹))) → (𝑥 ≠ 𝑦 → 𝑥 = 𝑦))
24	23	necon1bd 2943	. . . . 5 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹))) → (¬ 𝑥 = 𝑦 → 𝑥 = 𝑦))
25	24	pm2.18d 127	. . . 4 ⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹))) → 𝑥 = 𝑦)
26	25	ex 412	. . 3 ⊢ (𝐽 ∈ Haus → ((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) → 𝑥 = 𝑦))
27	26	alrimivv 1928	. 2 ⊢ (𝐽 ∈ Haus → ∀𝑥∀𝑦((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) → 𝑥 = 𝑦))
28		eleq1w 2811	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ 𝑦 ∈ (𝐽 fLim 𝐹)))
29	28	mo4 2559	. 2 ⊢ (∃*𝑥 𝑥 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐽 fLim 𝐹) ∧ 𝑦 ∈ (𝐽 fLim 𝐹)) → 𝑥 = 𝑦))
30	27, 29	sylibr 234	1 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝐹))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2109  ∃*wmo 2531   ≠ wne 2925  ∃wrex 3053   ∩ cin 3913  ∅c0 4296  ∪ cuni 4871  (class class class)co 7387  Hauscha 23195   fLim cflim 23821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-fbas 21261  df-top 22781  df-nei 22985  df-haus 23202  df-fil 23733  df-flim 23826

This theorem is referenced by:  hausflim  23868  hausflf  23884  metsscmetcld  25215  minveclem4a  25330