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

Theorem hausflim 21074
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  |-  X  = 
U. J
Assertion
Ref Expression
hausflim  |-  ( J  e.  Haus  <->  ( J  e. 
Top  /\  A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f ) ) )
Distinct variable groups:    x, f, J    f, X, x

Proof of Theorem hausflim
Dummy variables  v  u  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 haustop 20424 . . 3  |-  ( J  e.  Haus  ->  J  e. 
Top )
2 hausflimi 21073 . . . 4  |-  ( J  e.  Haus  ->  E* x  x  e.  ( J  fLim  f ) )
32ralrimivw 2810 . . 3  |-  ( J  e.  Haus  ->  A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f ) )
41, 3jca 541 . 2  |-  ( J  e.  Haus  ->  ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) ) )
5 simpl 464 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  J  e.  Top )
6 flimcf.1 . . . . . . . . . . . . . . 15  |-  X  = 
U. J
76toptopon 20025 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
85, 7sylib 201 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  J  e.  (TopOn `  X
) )
9 simprll 780 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
z  e.  X )
109snssd 4108 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { z }  C_  X )
11 snnzg 4080 . . . . . . . . . . . . . 14  |-  ( z  e.  X  ->  { z }  =/=  (/) )
129, 11syl 17 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { z }  =/=  (/) )
13 neifil 20973 . . . . . . . . . . . . 13  |-  ( ( J  e.  (TopOn `  X )  /\  {
z }  C_  X  /\  { z }  =/=  (/) )  ->  ( ( nei `  J ) `  { z } )  e.  ( Fil `  X
) )
148, 10, 12, 13syl3anc 1292 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { z } )  e.  ( Fil `  X ) )
15 filfbas 20941 . . . . . . . . . . . 12  |-  ( ( ( nei `  J
) `  { z } )  e.  ( Fil `  X )  ->  ( ( nei `  J ) `  {
z } )  e.  ( fBas `  X
) )
1614, 15syl 17 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { z } )  e.  (
fBas `  X )
)
17 simprlr 781 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  w  e.  X )
1817snssd 4108 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { w }  C_  X )
19 snnzg 4080 . . . . . . . . . . . . . 14  |-  ( w  e.  X  ->  { w }  =/=  (/) )
2017, 19syl 17 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { w }  =/=  (/) )
21 neifil 20973 . . . . . . . . . . . . 13  |-  ( ( J  e.  (TopOn `  X )  /\  {
w }  C_  X  /\  { w }  =/=  (/) )  ->  ( ( nei `  J ) `  { w } )  e.  ( Fil `  X
) )
228, 18, 20, 21syl3anc 1292 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { w } )  e.  ( Fil `  X ) )
23 filfbas 20941 . . . . . . . . . . . 12  |-  ( ( ( nei `  J
) `  { w } )  e.  ( Fil `  X )  ->  ( ( nei `  J ) `  {
w } )  e.  ( fBas `  X
) )
2422, 23syl 17 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { w } )  e.  (
fBas `  X )
)
25 fbunfip 20962 . . . . . . . . . . 11  |-  ( ( ( ( nei `  J
) `  { z } )  e.  (
fBas `  X )  /\  ( ( nei `  J
) `  { w } )  e.  (
fBas `  X )
)  ->  ( -.  (/) 
e.  ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) )  <->  A. u  e.  (
( nei `  J
) `  { z } ) A. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =/=  (/) ) )
2616, 24, 25syl2anc 673 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  <->  A. u  e.  (
( nei `  J
) `  { z } ) A. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =/=  (/) ) )
276neisspw 20200 . . . . . . . . . . . . . . 15  |-  ( J  e.  Top  ->  (
( nei `  J
) `  { z } )  C_  ~P X )
286neisspw 20200 . . . . . . . . . . . . . . 15  |-  ( J  e.  Top  ->  (
( nei `  J
) `  { w } )  C_  ~P X )
2927, 28unssd 3601 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  ->  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ~P X )
3029adantr 472 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) )  C_  ~P X )
3130a1d 25 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  ->  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) )  C_  ~P X ) )
32 ssun1 3588 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { z } )  C_  ( (
( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )
33 filn0 20955 . . . . . . . . . . . . . . 15  |-  ( ( ( nei `  J
) `  { z } )  e.  ( Fil `  X )  ->  ( ( nei `  J ) `  {
z } )  =/=  (/) )
3414, 33syl 17 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { z } )  =/=  (/) )
35 ssn0 3770 . . . . . . . . . . . . . 14  |-  ( ( ( ( nei `  J
) `  { z } )  C_  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  /\  ( ( nei `  J
) `  { z } )  =/=  (/) )  -> 
( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) )  =/=  (/) )
3632, 34, 35sylancr 676 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) )  =/=  (/) )
3736a1d 25 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  ->  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) )  =/=  (/) ) )
38 idd 24 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  ->  -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )
3931, 37, 383jcad 1211 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  ->  ( ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ~P X  /\  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) )
406topopn 20013 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  ->  X  e.  J )
4140adantr 472 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  X  e.  J )
42 fsubbas 20960 . . . . . . . . . . . . 13  |-  ( X  e.  J  ->  (
( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
)  <->  ( ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ~P X  /\  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) )
4341, 42syl 17 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
)  <->  ( ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ~P X  /\  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) )
44 fgcl 20971 . . . . . . . . . . . . . . 15  |-  ( ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
)  ->  ( X filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) )  e.  ( Fil `  X ) )
4544adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) )  e.  ( Fil `  X ) )
46 simplrr 779 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  z  =/=  w )
479adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  z  e.  X )
4817adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  w  e.  X )
49 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( nei `  J ) `
 { z } )  e.  _V
50 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( nei `  J ) `
 { w }
)  e.  _V
5149, 50unex 6608 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  e. 
_V
52 ssfii 7951 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  e. 
_V  ->  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) )  C_  ( fi `  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) ) )
5351, 52ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )
54 ssfg 20965 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
)  ->  ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) 
C_  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )
5554adantl 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  ( fi `  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )
5653, 55syl5ss 3429 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )
5732, 56syl5ss 3429 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  (
( nei `  J
) `  { z } )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )
588adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  J  e.  (TopOn `  X )
)
59 elflim 21064 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J  e.  (TopOn `  X )  /\  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) )  e.  ( Fil `  X ) )  -> 
( z  e.  ( J  fLim  ( X filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  <->  ( z  e.  X  /\  (
( nei `  J
) `  { z } )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )
6058, 45, 59syl2anc 673 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  (
z  e.  ( J 
fLim  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  <->  ( z  e.  X  /\  (
( nei `  J
) `  { z } )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )
6147, 57, 60mpbir2and 936 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  z  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) )
6256unssbd 3603 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  (
( nei `  J
) `  { w } )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )
63 elflim 21064 . . . . . . . . . . . . . . . . . . 19  |-  ( ( J  e.  (TopOn `  X )  /\  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) )  e.  ( Fil `  X ) )  -> 
( w  e.  ( J  fLim  ( X filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  <->  ( w  e.  X  /\  (
( nei `  J
) `  { w } )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )
6458, 45, 63syl2anc 673 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  (
w  e.  ( J 
fLim  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  <->  ( w  e.  X  /\  (
( nei `  J
) `  { w } )  C_  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )
6548, 62, 64mpbir2and 936 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  w  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) )
66 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
x  e.  ( J 
fLim  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  <->  z  e.  ( J  fLim  ( X
filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) ) )
67 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  w  ->  (
x  e.  ( J 
fLim  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  <->  w  e.  ( J  fLim  ( X
filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) ) )
6866, 67moi 3209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( z  e.  X  /\  w  e.  X
)  /\  E* x  x  e.  ( J  fLim  ( X filGen ( fi
`  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) ) ) )  /\  ( z  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )  /\  w  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )  ->  z  =  w )
69683com23 1237 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z  e.  X  /\  w  e.  X
)  /\  ( z  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )  /\  w  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) )  /\  E* x  x  e.  ( J  fLim  ( X
filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) )  -> 
z  =  w )
70693expia 1233 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  X  /\  w  e.  X
)  /\  ( z  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) )  /\  w  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )  ->  ( E* x  x  e.  ( J  fLim  ( X filGen ( fi
`  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) ) ) )  ->  z  =  w ) )
7147, 48, 61, 65, 70syl22anc 1293 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  ( E* x  x  e.  ( J  fLim  ( X
filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) )  ->  z  =  w ) )
7271necon3ad 2656 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  (
z  =/=  w  ->  -.  E* x  x  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )
7346, 72mpd 15 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  -.  E* x  x  e.  ( J  fLim  ( X
filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) )
74 oveq2 6316 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) )  ->  ( J  fLim  f )  =  ( J  fLim  ( X filGen ( fi `  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) )
7574eleq2d 2534 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) )  ->  ( x  e.  ( J  fLim  f
)  <->  x  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) ) ) ) )
7675mobidv 2340 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) )  ->  ( E* x  x  e.  ( J  fLim  f )  <->  E* x  x  e.  ( J  fLim  ( X filGen ( fi
`  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) ) ) ) ) )
7776notbid 301 . . . . . . . . . . . . . . 15  |-  ( f  =  ( X filGen ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) )  ->  ( -.  E* x  x  e.  ( J  fLim  f )  <->  -.  E* x  x  e.  ( J  fLim  ( X filGen ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) ) ) ) ) )
7877rspcev 3136 . . . . . . . . . . . . . 14  |-  ( ( ( X filGen ( fi
`  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) ) )  e.  ( Fil `  X
)  /\  -.  E* x  x  e.  ( J  fLim  ( X filGen ( fi
`  ( ( ( nei `  J ) `
 { z } )  u.  ( ( nei `  J ) `
 { w }
) ) ) ) ) )  ->  E. f  e.  ( Fil `  X
)  -.  E* x  x  e.  ( J  fLim  f ) )
7945, 73, 78syl2anc 673 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
) )  ->  E. f  e.  ( Fil `  X
)  -.  E* x  x  e.  ( J  fLim  f ) )
8079ex 441 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( fi `  ( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) ) )  e.  ( fBas `  X
)  ->  E. f  e.  ( Fil `  X
)  -.  E* x  x  e.  ( J  fLim  f ) ) )
8143, 80sylbird 243 . . . . . . . . . . 11  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ~P X  /\  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  =/=  (/)  /\  -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) ) )  ->  E. f  e.  ( Fil `  X
)  -.  E* x  x  e.  ( J  fLim  f ) ) )
8239, 81syld 44 . . . . . . . . . 10  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  (/)  e.  ( fi `  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) ) )  ->  E. f  e.  ( Fil `  X )  -.  E* x  x  e.  ( J  fLim  f ) ) )
8326, 82sylbird 243 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( A. u  e.  ( ( nei `  J
) `  { z } ) A. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =/=  (/)  ->  E. f  e.  ( Fil `  X )  -.  E* x  x  e.  ( J  fLim  f ) ) )
84 df-ne 2643 . . . . . . . . . . . . 13  |-  ( ( u  i^i  v )  =/=  (/)  <->  -.  ( u  i^i  v )  =  (/) )
8584ralbii 2823 . . . . . . . . . . . 12  |-  ( A. v  e.  ( ( nei `  J ) `  { w } ) ( u  i^i  v
)  =/=  (/)  <->  A. v  e.  ( ( nei `  J
) `  { w } )  -.  (
u  i^i  v )  =  (/) )
86 ralnex 2834 . . . . . . . . . . . 12  |-  ( A. v  e.  ( ( nei `  J ) `  { w } )  -.  ( u  i^i  v )  =  (/)  <->  -.  E. v  e.  ( ( nei `  J ) `
 { w }
) ( u  i^i  v )  =  (/) )
8785, 86bitri 257 . . . . . . . . . . 11  |-  ( A. v  e.  ( ( nei `  J ) `  { w } ) ( u  i^i  v
)  =/=  (/)  <->  -.  E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) )
8887ralbii 2823 . . . . . . . . . 10  |-  ( A. u  e.  ( ( nei `  J ) `  { z } ) A. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =/=  (/) 
<-> 
A. u  e.  ( ( nei `  J
) `  { z } )  -.  E. v  e.  ( ( nei `  J ) `  { w } ) ( u  i^i  v
)  =  (/) )
89 ralnex 2834 . . . . . . . . . 10  |-  ( A. u  e.  ( ( nei `  J ) `  { z } )  -.  E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) 
<->  -.  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) )
9088, 89bitri 257 . . . . . . . . 9  |-  ( A. u  e.  ( ( nei `  J ) `  { z } ) A. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =/=  (/) 
<->  -.  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) )
91 rexnal 2836 . . . . . . . . 9  |-  ( E. f  e.  ( Fil `  X )  -.  E* x  x  e.  ( J  fLim  f )  <->  -.  A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f ) )
9283, 90, 913imtr3g 277 . . . . . . . 8  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( -.  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/)  ->  -.  A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f ) ) )
9392con4d 108 . . . . . . 7  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f )  ->  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) ) )
9493imp 436 . . . . . 6  |-  ( ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  E. u  e.  (
( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) )
9594an32s 821 . . . . 5  |-  ( ( ( J  e.  Top  /\ 
A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f
) )  /\  (
( z  e.  X  /\  w  e.  X
)  /\  z  =/=  w ) )  ->  E. u  e.  (
( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) )
9695expr 626 . . . 4  |-  ( ( ( J  e.  Top  /\ 
A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f
) )  /\  (
z  e.  X  /\  w  e.  X )
)  ->  ( z  =/=  w  ->  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) ) )
9796ralrimivva 2814 . . 3  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  A. z  e.  X  A. w  e.  X  ( z  =/=  w  ->  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) ) )
98 simpl 464 . . . . 5  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  J  e.  Top )
9998, 7sylib 201 . . . 4  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  J  e.  (TopOn `  X
) )
100 hausnei2 20446 . . . 4  |-  ( J  e.  (TopOn `  X
)  ->  ( J  e.  Haus  <->  A. z  e.  X  A. w  e.  X  ( z  =/=  w  ->  E. u  e.  ( ( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) ) ) )
10199, 100syl 17 . . 3  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  -> 
( J  e.  Haus  <->  A. z  e.  X  A. w  e.  X  (
z  =/=  w  ->  E. u  e.  (
( nei `  J
) `  { z } ) E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) ) ) )
10297, 101mpbird 240 . 2  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  J  e.  Haus )
1034, 102impbii 192 1  |-  ( J  e.  Haus  <->  ( J  e. 
Top  /\  A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376    /\ w3a 1007    = wceq 1452    e. wcel 1904   E*wmo 2320    =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031    u. cun 3388    i^i cin 3389    C_ wss 3390   (/)c0 3722   ~Pcpw 3942   {csn 3959   U.cuni 4190   ` cfv 5589  (class class class)co 6308   ficfi 7942   fBascfbas 19035   filGencfg 19036   Topctop 19994  TopOnctopon 19995   neicnei 20190   Hauscha 20401   Filcfil 20938    fLim cflim 21027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-en 7588  df-fin 7591  df-fi 7943  df-fbas 19044  df-fg 19045  df-top 19998  df-topon 20000  df-nei 20191  df-haus 20408  df-fil 20939  df-flim 21032
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator