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

Metamath Proof Explorer

Theorem hausflim

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)

Ref Expression
Hypothesis flimcf.1 ⊢ 𝑋 = ∪ 𝐽
Assertion hausflim ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 flimcf.1 ⊢ 𝑋 = ∪ 𝐽
2 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
3 hausflimi ⊢ ( 𝐽 ∈ Haus → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
4 3 ralrimivw ⊢ ( 𝐽 ∈ Haus → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
5 2 4 jca ⊢ ( 𝐽 ∈ Haus → ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
6 simpl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → 𝐽 ∈ Top )
7 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
8 6 7 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 simprll ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → 𝑧 ∈ 𝑋 )
10 9 snssd ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → { 𝑧 } ⊆ 𝑋 )
11 9 snn0d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → { 𝑧 } ≠ ∅ )
12 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑧 } ⊆ 𝑋 ∧ { 𝑧 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( Fil ‘ 𝑋 ) )
13 8 10 11 12 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( Fil ‘ 𝑋 ) )
14 filfbas ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( Fil ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( fBas ‘ 𝑋 ) )
15 13 14 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( fBas ‘ 𝑋 ) )
16 simprlr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → 𝑤 ∈ 𝑋 )
17 16 snssd ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → { 𝑤 } ⊆ 𝑋 )
18 16 snn0d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → { 𝑤 } ≠ ∅ )
19 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑤 } ⊆ 𝑋 ∧ { 𝑤 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ ( Fil ‘ 𝑋 ) )
20 8 17 18 19 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ ( Fil ‘ 𝑋 ) )
21 filfbas ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ ( Fil ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ ( fBas ‘ 𝑋 ) )
22 20 21 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ ( fBas ‘ 𝑋 ) )
23 fbunfip ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( fBas ‘ 𝑋 ) ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ ( fBas ‘ 𝑋 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ↔ ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ ) )
24 15 22 23 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ↔ ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ ) )
25 1 neisspw ⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ⊆ 𝒫 𝑋 )
26 1 neisspw ⊢ ( 𝐽 ∈ Top → ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ⊆ 𝒫 𝑋 )
27 25 26 unssd ⊢ ( 𝐽 ∈ Top → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 )
28 27 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 )
29 28 a1d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 ) )
30 ssun1 ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ⊆ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) )
31 filn0 ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ ( Fil ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ≠ ∅ )
32 13 31 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ≠ ∅ )
33 ssn0 ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ⊆ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ≠ ∅ ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ )
34 30 32 33 sylancr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ )
35 34 a1d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ ) )
36 idd ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) → ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) )
37 29 35 36 3jcad ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) → ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
38 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
39 38 adantr ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → 𝑋 ∈ 𝐽 )
40 fsubbas ⊢ ( 𝑋 ∈ 𝐽 → ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
41 39 40 syl ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ↔ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
42 fgcl ⊢ ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) )
43 42 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) )
44 simplrr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → 𝑧 ≠ 𝑤 )
45 9 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
46 16 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → 𝑤 ∈ 𝑋 )
47 fvex ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∈ V
48 fvex ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ∈ V
49 47 48 unex ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ∈ V
50 ssfii ⊢ ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ∈ V → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) )
51 49 50 ax-mp ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) )
52 ssfg ⊢ ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) )
53 52 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) )
54 51 53 sstrid ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) )
55 30 54 sstrid ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) )
56 8 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
57 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
58 56 43 57 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
59 45 55 58 mpbir2and ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
60 54 unssbd ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) )
61 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
62 56 43 61 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ⊆ ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
63 46 60 62 mpbir2and ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
64 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ↔ 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
65 eleq1w ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ↔ 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
66 64 65 moi ⊢ ( ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ∧ ( 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ∧ 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) ) → 𝑧 = 𝑤 )
67 66 3com23 ⊢ ( ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ∧ 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) ∧ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) → 𝑧 = 𝑤 )
68 67 3expia ⊢ ( ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑧 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ∧ 𝑤 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) ) → ( ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) → 𝑧 = 𝑤 ) )
69 45 46 59 63 68 syl22anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) → 𝑧 = 𝑤 ) )
70 69 necon3ad ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑧 ≠ 𝑤 → ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
71 44 70 mpd ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
72 oveq2 ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) )
73 72 eleq2d ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ↔ 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
74 73 mobidv ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) → ( ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ↔ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
75 74 notbid ⊢ ( 𝑓 = ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) → ( ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ↔ ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) )
76 75 rspcev ⊢ ( ( ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ∈ ( Fil ‘ 𝑋 ) ∧ ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim ( 𝑋 filGen ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
77 43 71 76 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
78 77 ex ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ∈ ( fBas ‘ 𝑋 ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
79 41 78 sylbird ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ( ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ⊆ 𝒫 𝑋 ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ≠ ∅ ∧ ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
80 37 79 syld ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∅ ∈ ( fi ‘ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∪ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
81 24 80 sylbird ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
82 df-ne ⊢ ( ( 𝑢 ∩ 𝑣 ) ≠ ∅ ↔ ¬ ( 𝑢 ∩ 𝑣 ) = ∅ )
83 82 ralbii ⊢ ( ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ ↔ ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ¬ ( 𝑢 ∩ 𝑣 ) = ∅ )
84 ralnex ⊢ ( ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ¬ ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ¬ ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
85 83 84 bitri ⊢ ( ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ ↔ ¬ ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
86 85 ralbii ⊢ ( ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ ↔ ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ¬ ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
87 ralnex ⊢ ( ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ¬ ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ¬ ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
88 86 87 bitri ⊢ ( ∀ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∀ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) ≠ ∅ ↔ ¬ ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
89 rexnal ⊢ ( ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ¬ ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ↔ ¬ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
90 81 88 89 3imtr3g ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ¬ ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ → ¬ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
91 90 con4d ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
92 91 imp ⊢ ( ( ( 𝐽 ∈ Top ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
93 92 an32s ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑧 ≠ 𝑤 ) ) → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ )
94 93 expr ⊢ ( ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑧 ≠ 𝑤 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
95 94 ralrimivva ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝑧 ≠ 𝑤 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) )
96 simpl ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝐽 ∈ Top )
97 96 7 sylib ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
98 hausnei2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝑧 ≠ 𝑤 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
99 97 98 syl ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → ( 𝐽 ∈ Haus ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( 𝑧 ≠ 𝑤 → ∃ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑧 } ) ∃ 𝑣 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑤 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ) ) )
100 95 99 mpbird ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝐽 ∈ Haus )
101 5 100 impbii ⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )