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

Theorem hausflim 23990
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 23340 . . 3 (𝐽 ∈ Haus → 𝐽 ∈ Top)
2 hausflimi 23989 . . . 4 (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
32ralrimivw 3149 . . 3 (𝐽 ∈ Haus → ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
41, 3jca 511 . 2 (𝐽 ∈ Haus → (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
5 simpl 482 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝐽 ∈ Top)
6 flimcf.1 . . . . . . . . . . . . . . 15 𝑋 = 𝐽
76toptopon 22924 . . . . . . . . . . . . . 14 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
85, 7sylib 218 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝐽 ∈ (TopOn‘𝑋))
9 simprll 778 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝑧𝑋)
109snssd 4808 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑧} ⊆ 𝑋)
119snn0d 4774 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑧} ≠ ∅)
12 neifil 23889 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑧} ⊆ 𝑋 ∧ {𝑧} ≠ ∅) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
138, 10, 11, 12syl3anc 1372 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋))
14 filfbas 23857 . . . . . . . . . . . 12 (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
1513, 14syl 17 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋))
16 simprlr 779 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝑤𝑋)
1716snssd 4808 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑤} ⊆ 𝑋)
1816snn0d 4774 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → {𝑤} ≠ ∅)
19 neifil 23889 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑤} ⊆ 𝑋 ∧ {𝑤} ≠ ∅) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
208, 17, 18, 19syl3anc 1372 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋))
21 filfbas 23857 . . . . . . . . . . . 12 (((nei‘𝐽)‘{𝑤}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
2220, 21syl 17 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋))
23 fbunfip 23878 . . . . . . . . . . 11 ((((nei‘𝐽)‘{𝑧}) ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝑤}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅))
2415, 22, 23syl2anc 584 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅))
256neisspw 23116 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑧}) ⊆ 𝒫 𝑋)
266neisspw 23116 . . . . . . . . . . . . . . 15 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝑤}) ⊆ 𝒫 𝑋)
2725, 26unssd 4191 . . . . . . . . . . . . . 14 (𝐽 ∈ Top → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
2827adantr 480 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋)
2928a1d 25 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋))
30 ssun1 4177 . . . . . . . . . . . . . 14 ((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))
31 filn0 23871 . . . . . . . . . . . . . . 15 (((nei‘𝐽)‘{𝑧}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
3213, 31syl 17 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((nei‘𝐽)‘{𝑧}) ≠ ∅)
33 ssn0 4403 . . . . . . . . . . . . . 14 ((((nei‘𝐽)‘{𝑧}) ⊆ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∧ ((nei‘𝐽)‘{𝑧}) ≠ ∅) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
3430, 32, 33sylancr 587 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅)
3534a1d 25 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅))
36 idd 24 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
3729, 35, 363jcad 1129 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
386topopn 22913 . . . . . . . . . . . . . 14 (𝐽 ∈ Top → 𝑋𝐽)
3938adantr 480 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → 𝑋𝐽)
40 fsubbas 23876 . . . . . . . . . . . . 13 (𝑋𝐽 → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
4139, 40syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) ↔ ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
42 fgcl 23887 . . . . . . . . . . . . . . 15 ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
4342adantl 481 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋))
44 simplrr 777 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧𝑤)
459adantr 480 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧𝑋)
4616adantr 480 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤𝑋)
47 fvex 6918 . . . . . . . . . . . . . . . . . . . . . 22 ((nei‘𝐽)‘{𝑧}) ∈ V
48 fvex 6918 . . . . . . . . . . . . . . . . . . . . . 22 ((nei‘𝐽)‘{𝑤}) ∈ V
4947, 48unex 7765 . . . . . . . . . . . . . . . . . . . . 21 (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V
50 ssfii 9460 . . . . . . . . . . . . . . . . . . . . 21 ((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ∈ V → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))
5149, 50ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))
52 ssfg 23881 . . . . . . . . . . . . . . . . . . . . 21 ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
5352adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
5451, 53sstrid 3994 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
5530, 54sstrid 3994 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
568adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
57 elflim 23980 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
5856, 43, 57syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑧𝑋 ∧ ((nei‘𝐽)‘{𝑧}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
5945, 55, 58mpbir2and 713 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
6054unssbd 4193 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))
61 elflim 23980 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6256, 43, 61syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ (𝑤𝑋 ∧ ((nei‘𝐽)‘{𝑤}) ⊆ (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6346, 60, 62mpbir2and 713 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
64 eleq1w 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
65 eleq1w 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑤 → (𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ↔ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
6664, 65moi 3723 . . . . . . . . . . . . . . . . . . 19 (((𝑧𝑋𝑤𝑋) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → 𝑧 = 𝑤)
67663com23 1126 . . . . . . . . . . . . . . . . . 18 (((𝑧𝑋𝑤𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) ∧ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → 𝑧 = 𝑤)
68673expia 1121 . . . . . . . . . . . . . . . . 17 (((𝑧𝑋𝑤𝑋) ∧ (𝑧 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) ∧ 𝑤 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
6945, 46, 59, 63, 68syl22anc 838 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))) → 𝑧 = 𝑤))
7069necon3ad 2952 . . . . . . . . . . . . . . 15 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → (𝑧𝑤 → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7144, 70mpd 15 . . . . . . . . . . . . . 14 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
72 oveq2 7440 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝐽 fLim 𝑓) = (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))))))
7372eleq2d 2826 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7473mobidv 2548 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7574notbid 318 . . . . . . . . . . . . . . 15 (𝑓 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → (¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))))
7675rspcev 3621 . . . . . . . . . . . . . 14 (((𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) ∈ (Fil‘𝑋) ∧ ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen(fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
7743, 71, 76syl2anc 584 . . . . . . . . . . . . 13 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋)) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
7877ex 412 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ((fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) ∈ (fBas‘𝑋) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
7941, 78sylbird 260 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (((((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ⊆ 𝒫 𝑋 ∧ (((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤})))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
8037, 79syld 47 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∅ ∈ (fi‘(((nei‘𝐽)‘{𝑧}) ∪ ((nei‘𝐽)‘{𝑤}))) → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
8124, 80sylbird 260 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ → ∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
82 df-ne 2940 . . . . . . . . . . . . 13 ((𝑢𝑣) ≠ ∅ ↔ ¬ (𝑢𝑣) = ∅)
8382ralbii 3092 . . . . . . . . . . . 12 (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢𝑣) = ∅)
84 ralnex 3071 . . . . . . . . . . . 12 (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤}) ¬ (𝑢𝑣) = ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
8583, 84bitri 275 . . . . . . . . . . 11 (∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
8685ralbii 3092 . . . . . . . . . 10 (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
87 ralnex 3071 . . . . . . . . . 10 (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧}) ¬ ∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
8886, 87bitri 275 . . . . . . . . 9 (∀𝑢 ∈ ((nei‘𝐽)‘{𝑧})∀𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) ≠ ∅ ↔ ¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
89 rexnal 3099 . . . . . . . . 9 (∃𝑓 ∈ (Fil‘𝑋) ¬ ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) ↔ ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓))
9081, 88, 893imtr3g 295 . . . . . . . 8 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (¬ ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅ → ¬ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
9190con4d 115 . . . . . . 7 ((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → (∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅))
9291imp 406 . . . . . 6 (((𝐽 ∈ Top ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
9392an32s 652 . . . . 5 (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ ((𝑧𝑋𝑤𝑋) ∧ 𝑧𝑤)) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)
9493expr 456 . . . 4 (((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) ∧ (𝑧𝑋𝑤𝑋)) → (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅))
9594ralrimivva 3201 . . 3 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → ∀𝑧𝑋𝑤𝑋 (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅))
96 simpl 482 . . . . 5 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Top)
9796, 7sylib 218 . . . 4 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ (TopOn‘𝑋))
98 hausnei2 23362 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑧𝑋𝑤𝑋 (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)))
9997, 98syl 17 . . 3 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐽 ∈ Haus ↔ ∀𝑧𝑋𝑤𝑋 (𝑧𝑤 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑧})∃𝑣 ∈ ((nei‘𝐽)‘{𝑤})(𝑢𝑣) = ∅)))
10095, 99mpbird 257 . 2 ((𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)) → 𝐽 ∈ Haus)
1014, 100impbii 209 1 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  ∃*wmo 2537  wne 2939  wral 3060  wrex 3069  Vcvv 3479  cun 3948  cin 3949  wss 3950  c0 4332  𝒫 cpw 4599  {csn 4625   cuni 4906  cfv 6560  (class class class)co 7432  ficfi 9451  fBascfbas 21353  filGencfg 21354  Topctop 22900  TopOnctopon 22917  neicnei 23106  Hauscha 23317  Filcfil 23854   fLim cflim 23943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1o 8507  df-2o 8508  df-en 8987  df-fin 8990  df-fi 9452  df-fbas 21362  df-fg 21363  df-top 22901  df-topon 22918  df-nei 23107  df-haus 23324  df-fil 23855  df-flim 23948
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator