Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  neibastop2 Structured version   Unicode version

Theorem neibastop2 29780
Description: In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
neibastop1.1  |-  ( ph  ->  X  e.  V )
neibastop1.2  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
neibastop1.3  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
)  /\  w  e.  ( F `  x ) ) )  ->  (
( F `  x
)  i^i  ~P (
v  i^i  w )
)  =/=  (/) )
neibastop1.4  |-  J  =  { o  e.  ~P X  |  A. x  e.  o  ( ( F `  x )  i^i  ~P o )  =/=  (/) }
neibastop1.5  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
neibastop1.6  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
Assertion
Ref Expression
neibastop2  |-  ( (
ph  /\  P  e.  X )  ->  ( N  e.  ( ( nei `  J ) `  { P } )  <->  ( N  C_  X  /\  ( ( F `  P )  i^i  ~P N )  =/=  (/) ) ) )
Distinct variable groups:    v, t,
y, x    v, J    x, y, J    t, o,
v, w, x, y, P    o, N, t, v, w, x, y   
o, F, t, v, w, x, y    ph, o,
t, v, w, x, y    o, X, t, v, w, x, y
Allowed substitution hints:    J( w, t, o)    V( x, y, w, v, t, o)

Proof of Theorem neibastop2
Dummy variables  f  n  z  s  u  a  b  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neibastop1.1 . . . . . . . . 9  |-  ( ph  ->  X  e.  V )
2 neibastop1.2 . . . . . . . . 9  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
3 neibastop1.3 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
)  /\  w  e.  ( F `  x ) ) )  ->  (
( F `  x
)  i^i  ~P (
v  i^i  w )
)  =/=  (/) )
4 neibastop1.4 . . . . . . . . 9  |-  J  =  { o  e.  ~P X  |  A. x  e.  o  ( ( F `  x )  i^i  ~P o )  =/=  (/) }
51, 2, 3, 4neibastop1 29778 . . . . . . . 8  |-  ( ph  ->  J  e.  (TopOn `  X ) )
6 topontop 19191 . . . . . . . 8  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
75, 6syl 16 . . . . . . 7  |-  ( ph  ->  J  e.  Top )
87adantr 465 . . . . . 6  |-  ( (
ph  /\  P  e.  X )  ->  J  e.  Top )
9 eqid 2467 . . . . . . 7  |-  U. J  =  U. J
109neii1 19370 . . . . . 6  |-  ( ( J  e.  Top  /\  N  e.  ( ( nei `  J ) `  { P } ) )  ->  N  C_  U. J
)
118, 10sylan 471 . . . . 5  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  ->  N  C_  U. J )
12 toponuni 19192 . . . . . . 7  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
135, 12syl 16 . . . . . 6  |-  ( ph  ->  X  =  U. J
)
1413ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  ->  X  =  U. J )
1511, 14sseqtr4d 3541 . . . 4  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  ->  N  C_  X )
16 neii2 19372 . . . . . 6  |-  ( ( J  e.  Top  /\  N  e.  ( ( nei `  J ) `  { P } ) )  ->  E. y  e.  J  ( { P }  C_  y  /\  y  C_  N
) )
178, 16sylan 471 . . . . 5  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  ->  E. y  e.  J  ( { P }  C_  y  /\  y  C_  N
) )
18 pweq 4013 . . . . . . . . . . 11  |-  ( o  =  y  ->  ~P o  =  ~P y
)
1918ineq2d 3700 . . . . . . . . . 10  |-  ( o  =  y  ->  (
( F `  x
)  i^i  ~P o
)  =  ( ( F `  x )  i^i  ~P y ) )
2019neeq1d 2744 . . . . . . . . 9  |-  ( o  =  y  ->  (
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P y )  =/=  (/) ) )
2120raleqbi1dv 3066 . . . . . . . 8  |-  ( o  =  y  ->  ( A. x  e.  o 
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  A. x  e.  y  ( ( F `  x )  i^i  ~P y )  =/=  (/) ) )
2221, 4elrab2 3263 . . . . . . 7  |-  ( y  e.  J  <->  ( y  e.  ~P X  /\  A. x  e.  y  (
( F `  x
)  i^i  ~P y
)  =/=  (/) ) )
23 simprrr 764 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  y  C_  N
)
24 sspwb 4696 . . . . . . . . . . . . 13  |-  ( y 
C_  N  <->  ~P y  C_ 
~P N )
2523, 24sylib 196 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  ~P y  C_  ~P N )
26 sslin 3724 . . . . . . . . . . . 12  |-  ( ~P y  C_  ~P N  ->  ( ( F `  P )  i^i  ~P y )  C_  (
( F `  P
)  i^i  ~P N
) )
2725, 26syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  ( ( F `
 P )  i^i 
~P y )  C_  ( ( F `  P )  i^i  ~P N ) )
28 simprrl 763 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  { P }  C_  y )
29 snssg 4160 . . . . . . . . . . . . . 14  |-  ( P  e.  X  ->  ( P  e.  y  <->  { P }  C_  y ) )
3029ad3antlr 730 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  ( P  e.  y  <->  { P }  C_  y ) )
3128, 30mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  P  e.  y )
32 fveq2 5864 . . . . . . . . . . . . . . 15  |-  ( x  =  P  ->  ( F `  x )  =  ( F `  P ) )
3332ineq1d 3699 . . . . . . . . . . . . . 14  |-  ( x  =  P  ->  (
( F `  x
)  i^i  ~P y
)  =  ( ( F `  P )  i^i  ~P y ) )
3433neeq1d 2744 . . . . . . . . . . . . 13  |-  ( x  =  P  ->  (
( ( F `  x )  i^i  ~P y )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P y )  =/=  (/) ) )
3534rspcv 3210 . . . . . . . . . . . 12  |-  ( P  e.  y  ->  ( A. x  e.  y 
( ( F `  x )  i^i  ~P y )  =/=  (/)  ->  (
( F `  P
)  i^i  ~P y
)  =/=  (/) ) )
3631, 35syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  ( A. x  e.  y  ( ( F `  x )  i^i  ~P y )  =/=  (/)  ->  ( ( F `
 P )  i^i 
~P y )  =/=  (/) ) )
37 ssn0 3818 . . . . . . . . . . 11  |-  ( ( ( ( F `  P )  i^i  ~P y )  C_  (
( F `  P
)  i^i  ~P N
)  /\  ( ( F `  P )  i^i  ~P y )  =/=  (/) )  ->  ( ( F `  P )  i^i  ~P N )  =/=  (/) )
3827, 36, 37syl6an 545 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  ( y  e.  ~P X  /\  ( { P }  C_  y  /\  y  C_  N ) ) )  ->  ( A. x  e.  y  ( ( F `  x )  i^i  ~P y )  =/=  (/)  ->  ( ( F `
 P )  i^i 
~P N )  =/=  (/) ) )
3938expr 615 . . . . . . . . 9  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  y  e.  ~P X
)  ->  ( ( { P }  C_  y  /\  y  C_  N )  ->  ( A. x  e.  y  ( ( F `  x )  i^i  ~P y )  =/=  (/)  ->  ( ( F `
 P )  i^i 
~P N )  =/=  (/) ) ) )
4039com23 78 . . . . . . . 8  |-  ( ( ( ( ph  /\  P  e.  X )  /\  N  e.  (
( nei `  J
) `  { P } ) )  /\  y  e.  ~P X
)  ->  ( A. x  e.  y  (
( F `  x
)  i^i  ~P y
)  =/=  (/)  ->  (
( { P }  C_  y  /\  y  C_  N )  ->  (
( F `  P
)  i^i  ~P N
)  =/=  (/) ) ) )
4140expimpd 603 . . . . . . 7  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  -> 
( ( y  e. 
~P X  /\  A. x  e.  y  (
( F `  x
)  i^i  ~P y
)  =/=  (/) )  -> 
( ( { P }  C_  y  /\  y  C_  N )  ->  (
( F `  P
)  i^i  ~P N
)  =/=  (/) ) ) )
4222, 41syl5bi 217 . . . . . 6  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  -> 
( y  e.  J  ->  ( ( { P }  C_  y  /\  y  C_  N )  ->  (
( F `  P
)  i^i  ~P N
)  =/=  (/) ) ) )
4342rexlimdv 2953 . . . . 5  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  -> 
( E. y  e.  J  ( { P }  C_  y  /\  y  C_  N )  ->  (
( F `  P
)  i^i  ~P N
)  =/=  (/) ) )
4417, 43mpd 15 . . . 4  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  -> 
( ( F `  P )  i^i  ~P N )  =/=  (/) )
4515, 44jca 532 . . 3  |-  ( ( ( ph  /\  P  e.  X )  /\  N  e.  ( ( nei `  J
) `  { P } ) )  -> 
( N  C_  X  /\  ( ( F `  P )  i^i  ~P N )  =/=  (/) ) )
4645ex 434 . 2  |-  ( (
ph  /\  P  e.  X )  ->  ( N  e.  ( ( nei `  J ) `  { P } )  -> 
( N  C_  X  /\  ( ( F `  P )  i^i  ~P N )  =/=  (/) ) ) )
47 n0 3794 . . . 4  |-  ( ( ( F `  P
)  i^i  ~P N
)  =/=  (/)  <->  E. s 
s  e.  ( ( F `  P )  i^i  ~P N ) )
48 elin 3687 . . . . . 6  |-  ( s  e.  ( ( F `
 P )  i^i 
~P N )  <->  ( s  e.  ( F `  P
)  /\  s  e.  ~P N ) )
49 simprl 755 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  N  C_  X )
5013ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  X  =  U. J )
5149, 50sseqtrd 3540 . . . . . . . 8  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  N  C_  U. J )
521ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  X  e.  V )
532ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
54 simpll 753 . . . . . . . . . 10  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  ph )
5554, 3sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  ( s  e.  ( F `  P )  /\  s  e.  ~P N ) ) )  /\  ( x  e.  X  /\  v  e.  ( F `  x
)  /\  w  e.  ( F `  x ) ) )  ->  (
( F `  x
)  i^i  ~P (
v  i^i  w )
)  =/=  (/) )
56 neibastop1.5 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
5754, 56sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  ( s  e.  ( F `  P )  /\  s  e.  ~P N ) ) )  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
58 neibastop1.6 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
5954, 58sylan 471 . . . . . . . . 9  |-  ( ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  ( s  e.  ( F `  P )  /\  s  e.  ~P N ) ) )  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
60 simplr 754 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  P  e.  X )
61 simprrl 763 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  -> 
s  e.  ( F `
 P ) )
62 simprrr 764 . . . . . . . . . 10  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  -> 
s  e.  ~P N
)
6362elpwid 4020 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  -> 
s  C_  N )
64 fveq2 5864 . . . . . . . . . . . . . . . 16  |-  ( n  =  x  ->  ( F `  n )  =  ( F `  x ) )
6564ineq1d 3699 . . . . . . . . . . . . . . 15  |-  ( n  =  x  ->  (
( F `  n
)  i^i  ~P b
)  =  ( ( F `  x )  i^i  ~P b ) )
6665cbviunv 4364 . . . . . . . . . . . . . 14  |-  U_ n  e.  X  ( ( F `  n )  i^i  ~P b )  = 
U_ x  e.  X  ( ( F `  x )  i^i  ~P b )
67 pweq 4013 . . . . . . . . . . . . . . . 16  |-  ( b  =  z  ->  ~P b  =  ~P z
)
6867ineq2d 3700 . . . . . . . . . . . . . . 15  |-  ( b  =  z  ->  (
( F `  x
)  i^i  ~P b
)  =  ( ( F `  x )  i^i  ~P z ) )
6968iuneq2d 4352 . . . . . . . . . . . . . 14  |-  ( b  =  z  ->  U_ x  e.  X  ( ( F `  x )  i^i  ~P b )  = 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
7066, 69syl5eq 2520 . . . . . . . . . . . . 13  |-  ( b  =  z  ->  U_ n  e.  X  ( ( F `  n )  i^i  ~P b )  = 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
7170cbviunv 4364 . . . . . . . . . . . 12  |-  U_ b  e.  a  U_ n  e.  X  ( ( F `
 n )  i^i 
~P b )  = 
U_ z  e.  a 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z )
7271mpteq2i 4530 . . . . . . . . . . 11  |-  ( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  ( ( F `
 n )  i^i 
~P b ) )  =  ( a  e. 
_V  |->  U_ z  e.  a 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
73 rdgeq1 7074 . . . . . . . . . . 11  |-  ( ( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  (
( F `  n
)  i^i  ~P b
) )  =  ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) )  ->  rec ( ( a  e. 
_V  |->  U_ b  e.  a 
U_ n  e.  X  ( ( F `  n )  i^i  ~P b ) ) ,  { s } )  =  rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  {
s } ) )
7472, 73ax-mp 5 . . . . . . . . . 10  |-  rec (
( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  (
( F `  n
)  i^i  ~P b
) ) ,  {
s } )  =  rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z ) ) ,  { s } )
7574reseq1i 5267 . . . . . . . . 9  |-  ( rec ( ( a  e. 
_V  |->  U_ b  e.  a 
U_ n  e.  X  ( ( F `  n )  i^i  ~P b ) ) ,  { s } )  |`  om )  =  ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z ) ) ,  { s } )  |`  om )
76 pweq 4013 . . . . . . . . . . . . . 14  |-  ( g  =  f  ->  ~P g  =  ~P f
)
7776ineq2d 3700 . . . . . . . . . . . . 13  |-  ( g  =  f  ->  (
( F `  w
)  i^i  ~P g
)  =  ( ( F `  w )  i^i  ~P f ) )
7877neeq1d 2744 . . . . . . . . . . . 12  |-  ( g  =  f  ->  (
( ( F `  w )  i^i  ~P g )  =/=  (/)  <->  ( ( F `  w )  i^i  ~P f )  =/=  (/) ) )
7978cbvrexv 3089 . . . . . . . . . . 11  |-  ( E. g  e.  U. ran  ( rec ( ( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  ( ( F `
 n )  i^i 
~P b ) ) ,  { s } )  |`  om )
( ( F `  w )  i^i  ~P g )  =/=  (/)  <->  E. f  e.  U. ran  ( rec ( ( a  e. 
_V  |->  U_ b  e.  a 
U_ n  e.  X  ( ( F `  n )  i^i  ~P b ) ) ,  { s } )  |`  om ) ( ( F `  w )  i^i  ~P f )  =/=  (/) )
80 fveq2 5864 . . . . . . . . . . . . . 14  |-  ( w  =  y  ->  ( F `  w )  =  ( F `  y ) )
8180ineq1d 3699 . . . . . . . . . . . . 13  |-  ( w  =  y  ->  (
( F `  w
)  i^i  ~P f
)  =  ( ( F `  y )  i^i  ~P f ) )
8281neeq1d 2744 . . . . . . . . . . . 12  |-  ( w  =  y  ->  (
( ( F `  w )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )
8382rexbidv 2973 . . . . . . . . . . 11  |-  ( w  =  y  ->  ( E. f  e.  U. ran  ( rec ( ( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  ( ( F `
 n )  i^i 
~P b ) ) ,  { s } )  |`  om )
( ( F `  w )  i^i  ~P f )  =/=  (/)  <->  E. f  e.  U. ran  ( rec ( ( a  e. 
_V  |->  U_ b  e.  a 
U_ n  e.  X  ( ( F `  n )  i^i  ~P b ) ) ,  { s } )  |`  om ) ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )
8479, 83syl5bb 257 . . . . . . . . . 10  |-  ( w  =  y  ->  ( E. g  e.  U. ran  ( rec ( ( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  ( ( F `
 n )  i^i 
~P b ) ) ,  { s } )  |`  om )
( ( F `  w )  i^i  ~P g )  =/=  (/)  <->  E. f  e.  U. ran  ( rec ( ( a  e. 
_V  |->  U_ b  e.  a 
U_ n  e.  X  ( ( F `  n )  i^i  ~P b ) ) ,  { s } )  |`  om ) ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )
8584cbvrabv 3112 . . . . . . . . 9  |-  { w  e.  X  |  E. g  e.  U. ran  ( rec ( ( a  e. 
_V  |->  U_ b  e.  a 
U_ n  e.  X  ( ( F `  n )  i^i  ~P b ) ) ,  { s } )  |`  om ) ( ( F `  w )  i^i  ~P g )  =/=  (/) }  =  {
y  e.  X  |  E. f  e.  U. ran  ( rec ( ( a  e.  _V  |->  U_ b  e.  a  U_ n  e.  X  ( ( F `
 n )  i^i 
~P b ) ) ,  { s } )  |`  om )
( ( F `  y )  i^i  ~P f )  =/=  (/) }
8652, 53, 55, 4, 57, 59, 60, 49, 61, 63, 75, 85neibastop2lem 29779 . . . . . . . 8  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
877ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  J  e.  Top )
8860, 50eleqtrd 2557 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  P  e.  U. J )
899isneip 19369 . . . . . . . . 9  |-  ( ( J  e.  Top  /\  P  e.  U. J )  ->  ( N  e.  ( ( nei `  J
) `  { P } )  <->  ( N  C_ 
U. J  /\  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) ) ) )
9087, 88, 89syl2anc 661 . . . . . . . 8  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  -> 
( N  e.  ( ( nei `  J
) `  { P } )  <->  ( N  C_ 
U. J  /\  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) ) ) )
9151, 86, 90mpbir2and 920 . . . . . . 7  |-  ( ( ( ph  /\  P  e.  X )  /\  ( N  C_  X  /\  (
s  e.  ( F `
 P )  /\  s  e.  ~P N
) ) )  ->  N  e.  ( ( nei `  J ) `  { P } ) )
9291expr 615 . . . . . 6  |-  ( ( ( ph  /\  P  e.  X )  /\  N  C_  X )  ->  (
( s  e.  ( F `  P )  /\  s  e.  ~P N )  ->  N  e.  ( ( nei `  J
) `  { P } ) ) )
9348, 92syl5bi 217 . . . . 5  |-  ( ( ( ph  /\  P  e.  X )  /\  N  C_  X )  ->  (
s  e.  ( ( F `  P )  i^i  ~P N )  ->  N  e.  ( ( nei `  J
) `  { P } ) ) )
9493exlimdv 1700 . . . 4  |-  ( ( ( ph  /\  P  e.  X )  /\  N  C_  X )  ->  ( E. s  s  e.  ( ( F `  P )  i^i  ~P N )  ->  N  e.  ( ( nei `  J
) `  { P } ) ) )
9547, 94syl5bi 217 . . 3  |-  ( ( ( ph  /\  P  e.  X )  /\  N  C_  X )  ->  (
( ( F `  P )  i^i  ~P N )  =/=  (/)  ->  N  e.  ( ( nei `  J
) `  { P } ) ) )
9695expimpd 603 . 2  |-  ( (
ph  /\  P  e.  X )  ->  (
( N  C_  X  /\  ( ( F `  P )  i^i  ~P N )  =/=  (/) )  ->  N  e.  ( ( nei `  J ) `  { P } ) ) )
9746, 96impbid 191 1  |-  ( (
ph  /\  P  e.  X )  ->  ( N  e.  ( ( nei `  J ) `  { P } )  <->  ( N  C_  X  /\  ( ( F `  P )  i^i  ~P N )  =/=  (/) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379   E.wex 1596    e. wcel 1767    =/= wne 2662   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113    \ cdif 3473    i^i cin 3475    C_ wss 3476   (/)c0 3785   ~Pcpw 4010   {csn 4027   U.cuni 4245   U_ciun 4325    |-> cmpt 4505   ran crn 5000    |` cres 5001   -->wf 5582   ` cfv 5586   omcom 6678   reccrdg 7072   Topctop 19158  TopOnctopon 19159   neicnei 19361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-om 6679  df-recs 7039  df-rdg 7073  df-top 19163  df-topon 19166  df-nei 19362
This theorem is referenced by:  neibastop3  29781
  Copyright terms: Public domain W3C validator