MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hausflim Structured version   Visualization version   GIF version

Theorem hausflim 22006
Description: A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
Hypothesis
Ref Expression
flimcf.1 𝑋 = 𝐽
Assertion
Ref Expression
hausflim (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
Distinct variable groups:   𝑥,𝑓,𝐽   𝑓,𝑋,𝑥

Proof of Theorem hausflim
Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 haustop 21357 . . 3 (𝐽 ∈ Haus → 𝐽 ∈ Top)
2 hausflimi 22005 . . . 4 (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
32ralrimivw 3116 . . 3 (𝐽 ∈ Haus → ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
41, 3jca 497 . 2 (𝐽 ∈ Haus → (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
5 simpl 468 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝐽 ∈ Top)
6 flimcf.1 . . . . . . . . . . . . . . 15 𝑋 = 𝐽
76toptopon 20943 . . . . . . . . . . . . . 14 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 208 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝐽 ∈ (TopOn‘𝑋))
9 simprll 758 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝑧𝑋)
109snssd 4476 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑧} ⊆ 𝑋)
11 snnzg 4444 . . . . . . . . . . . . . 14 (𝑧𝑋 → {𝑧} ≠ ∅)
129, 11syl 17 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑧} ≠ ∅)
13 neifil 21905 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑧} ⊆ 𝑋 ∧ {𝑧} ≠ ∅) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
148, 10, 12, 13syl3anc 1476 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
15 filfbas 21873 . . . . . . . . . . . 12 (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
1614, 15syl 17 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
17 simprlr 759 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝑤𝑋)
1817snssd 4476 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑤} ⊆ 𝑋)
19 snnzg 4444 . . . . . . . . . . . . . 14 (𝑤𝑋 → {𝑤} ≠ ∅)
2017, 19syl 17 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑤} ≠ ∅)
21 neifil 21905 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑤} ⊆ 𝑋 ∧ {𝑤} ≠ ∅) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
228, 18, 20, 21syl3anc 1476 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
23 filfbas 21873 . . . . . . . . . . . 12 (((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
2422, 23syl 17 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
25 fbunfip 21894 . . . . . . . . . . 11 ((((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅))
2616, 24, 25syl2anc 567 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅))
276neisspw 21133 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑧}) ⊆ 𝒫 𝑋)
286neisspw 21133 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑤}) ⊆ 𝒫 𝑋)
2927, 28unssd 3941 . . . . . . . . . . . . . 14 (𝐽 ∈ Top → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
3029adantr 466 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
3130a1d 25 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋))
32 ssun1 3928 . . . . . . . . . . . . . 14 ((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))
33 filn0 21887 . . . . . . . . . . . . . . 15 (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
3414, 33syl 17 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
35 ssn0 4121 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∧ ((nei‘𝐽)‘{𝑧}) ≠ ∅) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
3632, 34, 35sylancr 569 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
3736a1d 25 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅))
38 idd 24 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
3931, 37, 383jcad 1123 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
406topopn 20932 . . . . . . . . . . . . . 14 (𝐽 ∈ Top → 𝑋𝐽)
4140adantr 466 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝑋𝐽)
42 fsubbas 21892 . . . . . . . . . . . . 13 (𝑋𝐽 → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
4341, 42syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
44 fgcl 21903 . . . . . . . . . . . . . . 15 ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
4544adantl 467 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
46 simplrr 757 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧𝑤)
479adantr 466 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧𝑋)
4817adantr 466 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤𝑋)
49 fvex 6343 . . . . . . . . . . . . . . . . . . . . . 22 ((nei‘𝐽)‘{𝑧}) ∈ V
50 fvex 6343 . . . . . . . . . . . . . . . . . . . . . 22 ((nei‘𝐽)‘{𝑤}) ∈ V
5149, 50unex 7104 . . . . . . . . . . . . . . . . . . . . 21 (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V
52 ssfii 8482 . . . . . . . . . . . . . . . . . . . . 21 ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))
5351, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))
54 ssfg 21897 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
5554adantl 467 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
5653, 55syl5ss 3764 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
5732, 56syl5ss 3764 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
588adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
59 elflim 21996 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6058, 45, 59syl2anc 567 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6147, 57, 60mpbir2and 686 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
6256unssbd 3943 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
63 elflim 21996 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6458, 45, 63syl2anc 567 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6548, 62, 64mpbir2and 686 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
66 eleq1w 2833 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
67 eleq1w 2833 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6866, 67moi 3542 . . . . . . . . . . . . . . . . . . 19 (((𝑧𝑋𝑤𝑋) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → 𝑧 = 𝑤)
69683com23 1120 . . . . . . . . . . . . . . . . . 18 (((𝑧𝑋𝑤𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → 𝑧 = 𝑤)
70693expia 1114 . . . . . . . . . . . . . . . . 17 (((𝑧𝑋𝑤𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
7147, 48, 61, 65, 70syl22anc 1477 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
7271necon3ad 2956 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧𝑤 → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7346, 72mpd 15 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
74 oveq2 6802 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝐽 fLim 𝑓) = (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
7574eleq2d 2836 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7675mobidv 2639 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7776notbid 307 . . . . . . . . . . . . . . 15 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7877rspcev 3461 . . . . . . . . . . . . . 14 (((𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋) ∧ ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
7945, 73, 78syl2anc 567 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
8079ex 397 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
8143, 80sylbird 250 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
8239, 81syld 47 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
8326, 82sylbird 250 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
84 df-ne 2944 . . . . . . . . . . . . 13 ((𝑢𝑣) ≠ ∅ ↔ ¬ (𝑢𝑣) = ∅)
8584ralbii 3129 . . . . . . . . . . . 12 (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢𝑣) = ∅)
86 ralnex 3141 . . . . . . . . . . . 12 (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢𝑣) = ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
8785, 86bitri 264 . . . . . . . . . . 11 (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
8887ralbii 3129 . . . . . . . . . 10 (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
89 ralnex 3141 . . . . . . . . . 10 (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
9088, 89bitri 264 . . . . . . . . 9 (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
91 rexnal 3143 . . . . . . . . 9 (∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
9283, 90, 913imtr3g 284 . . . . . . . 8 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅ → ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
9392con4d 115 . . . . . . 7 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅))
9493imp 393 . . . . . 6 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
9594an32s 625 . . . . 5 (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
9695expr 444 . . . 4 (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ (𝑧𝑋𝑤𝑋)) → (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅))
9796ralrimivva 3120 . . 3 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∀𝑧𝑋𝑤𝑋 (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅))
98 simpl 468 . . . . 5 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Top)
9998, 7sylib 208 . . . 4 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ (TopOn‘𝑋))
100 hausnei2 21379 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑧𝑋𝑤𝑋 (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)))
10199, 100syl 17 . . 3 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐽 ∈ Haus ↔ ∀𝑧𝑋𝑤𝑋 (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)))
10297, 101mpbird 247 . 2 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Haus)
1034, 102impbii 199 1 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  ∃*wmo 2619  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cun 3722  cin 3723  wss 3724  c0 4064  𝒫 cpw 4298  {csn 4317   cuni 4575  cfv 6032  (class class class)co 6794  ficfi 8473  fBascfbas 19950  filGencfg 19951  Topctop 20919  TopOnctopon 20936  neicnei 21123  Hauscha 21334  Filcfil 21870   fLim cflim 21959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-en 8111  df-fin 8114  df-fi 8474  df-fbas 19959  df-fg 19960  df-top 20920  df-topon 20937  df-nei 21124  df-haus 21341  df-fil 21871  df-flim 21964
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator