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

Metamath Proof Explorer

Theorem hausflim

Proof