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

Theorem hausflim 20995
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 20346 . . 3  |-  ( J  e.  Haus  ->  J  e. 
Top )
2 hausflimi 20994 . . . 4  |-  ( J  e.  Haus  ->  E* x  x  e.  ( J  fLim  f ) )
32ralrimivw 2837 . . 3  |-  ( J  e.  Haus  ->  A. f  e.  ( Fil `  X
) E* x  x  e.  ( J  fLim  f ) )
41, 3jca 534 . 2  |-  ( J  e.  Haus  ->  ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) ) )
5 simpl 458 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  J  e.  Top )
6 flimcf.1 . . . . . . . . . . . . . . 15  |-  X  = 
U. J
76toptopon 19947 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  <->  J  e.  (TopOn `  X ) )
85, 7sylib 199 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  J  e.  (TopOn `  X
) )
9 simprll 770 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
z  e.  X )
109snssd 4145 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { z }  C_  X )
11 snnzg 4117 . . . . . . . . . . . . . 14  |-  ( z  e.  X  ->  { z }  =/=  (/) )
129, 11syl 17 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { z }  =/=  (/) )
13 neifil 20894 . . . . . . . . . . . . 13  |-  ( ( J  e.  (TopOn `  X )  /\  {
z }  C_  X  /\  { z }  =/=  (/) )  ->  ( ( nei `  J ) `  { z } )  e.  ( Fil `  X
) )
148, 10, 12, 13syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { z } )  e.  ( Fil `  X ) )
15 filfbas 20862 . . . . . . . . . . . 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 771 . . . . . . . . . . . . . 14  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  w  e.  X )
1817snssd 4145 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { w }  C_  X )
19 snnzg 4117 . . . . . . . . . . . . . 14  |-  ( w  e.  X  ->  { w }  =/=  (/) )
2017, 19syl 17 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  { w }  =/=  (/) )
21 neifil 20894 . . . . . . . . . . . . 13  |-  ( ( J  e.  (TopOn `  X )  /\  {
w }  C_  X  /\  { w }  =/=  (/) )  ->  ( ( nei `  J ) `  { w } )  e.  ( Fil `  X
) )
228, 18, 20, 21syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( nei `  J
) `  { w } )  e.  ( Fil `  X ) )
23 filfbas 20862 . . . . . . . . . . . 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 20883 . . . . . . . . . . 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 665 . . . . . . . . . 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 20122 . . . . . . . . . . . . . . 15  |-  ( J  e.  Top  ->  (
( nei `  J
) `  { z } )  C_  ~P X )
286neisspw 20122 . . . . . . . . . . . . . . 15  |-  ( J  e.  Top  ->  (
( nei `  J
) `  { w } )  C_  ~P X )
2927, 28unssd 3642 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  ->  (
( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  C_  ~P X )
3029adantr 466 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) )  C_  ~P X )
3130a1d 26 . . . . . . . . . . . 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 3629 . . . . . . . . . . . . . 14  |-  ( ( nei `  J ) `
 { z } )  C_  ( (
( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )
33 filn0 20876 . . . . . . . . . . . . . . 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 3797 . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  -> 
( ( ( nei `  J ) `  {
z } )  u.  ( ( nei `  J
) `  { w } ) )  =/=  (/) )
3736a1d 26 . . . . . . . . . . . 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 25 . . . . . . . . . . . 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 1186 . . . . . . . . . . 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 19935 . . . . . . . . . . . . . 14  |-  ( J  e.  Top  ->  X  e.  J )
4140adantr 466 . . . . . . . . . . . . 13  |-  ( ( J  e.  Top  /\  ( ( z  e.  X  /\  w  e.  X )  /\  z  =/=  w ) )  ->  X  e.  J )
42 fsubbas 20881 . . . . . . . . . . . . 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 20892 . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . 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 5892 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( nei `  J ) `
 { z } )  e.  _V
50 fvex 5892 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( nei `  J ) `
 { w }
)  e.  _V
5149, 50unex 6604 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( nei `  J
) `  { z } )  u.  (
( nei `  J
) `  { w } ) )  e. 
_V
52 ssfii 7943 . . . . . . . . . . . . . . . . . . . . 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 20886 . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . 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 3475 . . . . . . . . . . . . . . . . . . 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 3475 . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . 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 20985 . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . 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 930 . . . . . . . . . . . . . . . . 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 3644 . . . . . . . . . . . . . . . . . 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 20985 . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . 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 930 . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . . . 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 3253 . . . . . . . . . . . . . . . . . . 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 1211 . . . . . . . . . . . . . . . . . 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 1207 . . . . . . . . . . . . . . . . 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 1265 . . . . . . . . . . . . . . . 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 2630 . . . . . . . . . . . . . . 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 6314 . . . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . . . 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 2290 . . . . . . . . . . . . . . . 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 295 . . . . . . . . . . . . . . 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 3182 . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . 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 435 . . . . . . . . . . . 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 238 . . . . . . . . . . 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 45 . . . . . . . . . 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 238 . . . . . . . . 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 2616 . . . . . . . . . . . . 13  |-  ( ( u  i^i  v )  =/=  (/)  <->  -.  ( u  i^i  v )  =  (/) )
8584ralbii 2853 . . . . . . . . . . . 12  |-  ( A. v  e.  ( ( nei `  J ) `  { w } ) ( u  i^i  v
)  =/=  (/)  <->  A. v  e.  ( ( nei `  J
) `  { w } )  -.  (
u  i^i  v )  =  (/) )
86 ralnex 2868 . . . . . . . . . . . 12  |-  ( A. v  e.  ( ( nei `  J ) `  { w } )  -.  ( u  i^i  v )  =  (/)  <->  -.  E. v  e.  ( ( nei `  J ) `
 { w }
) ( u  i^i  v )  =  (/) )
8785, 86bitri 252 . . . . . . . . . . 11  |-  ( A. v  e.  ( ( nei `  J ) `  { w } ) ( u  i^i  v
)  =/=  (/)  <->  -.  E. v  e.  ( ( nei `  J
) `  { w } ) ( u  i^i  v )  =  (/) )
8887ralbii 2853 . . . . . . . . . 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 2868 . . . . . . . . . 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 252 . . . . . . . . 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 2870 . . . . . . . . 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 272 . . . . . . . 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 430 . . . . . 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 811 . . . . 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 618 . . . 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 2843 . . 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 458 . . . . 5  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  J  e.  Top )
9998, 7sylib 199 . . . 4  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  J  e.  (TopOn `  X
) )
100 hausnei2 20368 . . . 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 235 . 2  |-  ( ( J  e.  Top  /\  A. f  e.  ( Fil `  X ) E* x  x  e.  ( J  fLim  f ) )  ->  J  e.  Haus )
1034, 102impbii 190 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 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   E*wmo 2270    =/= wne 2614   A.wral 2771   E.wrex 2772   _Vcvv 3080    u. cun 3434    i^i cin 3435    C_ wss 3436   (/)c0 3761   ~Pcpw 3981   {csn 3998   U.cuni 4219   ` cfv 5601  (class class class)co 6306   ficfi 7934   fBascfbas 18958   filGencfg 18959   Topctop 19916  TopOnctopon 19917   neicnei 20112   Hauscha 20323   Filcfil 20859    fLim cflim 20948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-oadd 7198  df-er 7375  df-en 7582  df-fin 7585  df-fi 7935  df-fbas 18967  df-fg 18968  df-top 19920  df-topon 19922  df-nei 20113  df-haus 20330  df-fil 20860  df-flim 20953
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator