Metamath Proof Explorer

Theorem neips

Description: A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 16-Nov-2006)

Ref Expression
Hypothesis neips.1 
|- X = U. J
Assertion neips 
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( N e. ( ( nei ` J ) ` S ) <-> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )

Proof

Step Hyp Ref Expression
1 neips.1 
 |-  X = U. J
2 snssi 
 |-  ( p e. S -> { p } C_ S )
3 neiss 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ { p } C_ S ) -> N e. ( ( nei ` J ) ` { p } ) )
4 2 3 syl3an3 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ p e. S ) -> N e. ( ( nei ` J ) ` { p } ) )
5 4 3exp 
 |-  ( J e. Top -> ( N e. ( ( nei ` J ) ` S ) -> ( p e. S -> N e. ( ( nei ` J ) ` { p } ) ) ) )
6 5 ralrimdv 
 |-  ( J e. Top -> ( N e. ( ( nei ` J ) ` S ) -> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )
7 6 3ad2ant1 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( N e. ( ( nei ` J ) ` S ) -> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )
8 r19.28zv 
 |-  ( S =/= (/) -> ( A. p e. S ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) <-> ( N C_ X /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) ) )
9 8 3ad2ant3 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( A. p e. S ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) <-> ( N C_ X /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) ) )
10 ssrab2 
 |-  { v e. J | v C_ N } C_ J
11 uniopn 
 |-  ( ( J e. Top /\ { v e. J | v C_ N } C_ J ) -> U. { v e. J | v C_ N } e. J )
12 10 11 mpan2 
 |-  ( J e. Top -> U. { v e. J | v C_ N } e. J )
13 12 ad2antrr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) -> U. { v e. J | v C_ N } e. J )
14 sseq1 
 |-  ( v = g -> ( v C_ N <-> g C_ N ) )
15 14 elrab 
 |-  ( g e. { v e. J | v C_ N } <-> ( g e. J /\ g C_ N ) )
16 elunii 
 |-  ( ( p e. g /\ g e. { v e. J | v C_ N } ) -> p e. U. { v e. J | v C_ N } )
17 15 16 sylan2br 
 |-  ( ( p e. g /\ ( g e. J /\ g C_ N ) ) -> p e. U. { v e. J | v C_ N } )
18 17 an12s 
 |-  ( ( g e. J /\ ( p e. g /\ g C_ N ) ) -> p e. U. { v e. J | v C_ N } )
19 18 rexlimiva 
 |-  ( E. g e. J ( p e. g /\ g C_ N ) -> p e. U. { v e. J | v C_ N } )
20 19 ralimi 
 |-  ( A. p e. S E. g e. J ( p e. g /\ g C_ N ) -> A. p e. S p e. U. { v e. J | v C_ N } )
21 dfss3 
 |-  ( S C_ U. { v e. J | v C_ N } <-> A. p e. S p e. U. { v e. J | v C_ N } )
22 20 21 sylibr 
 |-  ( A. p e. S E. g e. J ( p e. g /\ g C_ N ) -> S C_ U. { v e. J | v C_ N } )
23 22 adantl 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) -> S C_ U. { v e. J | v C_ N } )
24 unissb 
 |-  ( U. { v e. J | v C_ N } C_ N <-> A. h e. { v e. J | v C_ N } h C_ N )
25 sseq1 
 |-  ( v = h -> ( v C_ N <-> h C_ N ) )
26 25 elrab 
 |-  ( h e. { v e. J | v C_ N } <-> ( h e. J /\ h C_ N ) )
27 26 simprbi 
 |-  ( h e. { v e. J | v C_ N } -> h C_ N )
28 24 27 mprgbir 
 |-  U. { v e. J | v C_ N } C_ N
29 23 28 jctir 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) -> ( S C_ U. { v e. J | v C_ N } /\ U. { v e. J | v C_ N } C_ N ) )
30 sseq2 
 |-  ( h = U. { v e. J | v C_ N } -> ( S C_ h <-> S C_ U. { v e. J | v C_ N } ) )
31 sseq1 
 |-  ( h = U. { v e. J | v C_ N } -> ( h C_ N <-> U. { v e. J | v C_ N } C_ N ) )
32 30 31 anbi12d 
 |-  ( h = U. { v e. J | v C_ N } -> ( ( S C_ h /\ h C_ N ) <-> ( S C_ U. { v e. J | v C_ N } /\ U. { v e. J | v C_ N } C_ N ) ) )
33 32 rspcev 
 |-  ( ( U. { v e. J | v C_ N } e. J /\ ( S C_ U. { v e. J | v C_ N } /\ U. { v e. J | v C_ N } C_ N ) ) -> E. h e. J ( S C_ h /\ h C_ N ) )
34 13 29 33 syl2anc 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) -> E. h e. J ( S C_ h /\ h C_ N ) )
35 34 ex 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A. p e. S E. g e. J ( p e. g /\ g C_ N ) -> E. h e. J ( S C_ h /\ h C_ N ) ) )
36 35 anim2d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( N C_ X /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) -> ( N C_ X /\ E. h e. J ( S C_ h /\ h C_ N ) ) ) )
37 36 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( N C_ X /\ A. p e. S E. g e. J ( p e. g /\ g C_ N ) ) -> ( N C_ X /\ E. h e. J ( S C_ h /\ h C_ N ) ) ) )
38 9 37 sylbid 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( A. p e. S ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) -> ( N C_ X /\ E. h e. J ( S C_ h /\ h C_ N ) ) ) )
39 ssel2 
 |-  ( ( S C_ X /\ p e. S ) -> p e. X )
40 1 isneip 
 |-  ( ( J e. Top /\ p e. X ) -> ( N e. ( ( nei ` J ) ` { p } ) <-> ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) ) )
41 39 40 sylan2 
 |-  ( ( J e. Top /\ ( S C_ X /\ p e. S ) ) -> ( N e. ( ( nei ` J ) ` { p } ) <-> ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) ) )
42 41 anassrs 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ p e. S ) -> ( N e. ( ( nei ` J ) ` { p } ) <-> ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) ) )
43 42 ralbidva 
 |-  ( ( J e. Top /\ S C_ X ) -> ( A. p e. S N e. ( ( nei ` J ) ` { p } ) <-> A. p e. S ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) ) )
44 43 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( A. p e. S N e. ( ( nei ` J ) ` { p } ) <-> A. p e. S ( N C_ X /\ E. g e. J ( p e. g /\ g C_ N ) ) ) )
45 1 isnei 
 |-  ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. h e. J ( S C_ h /\ h C_ N ) ) ) )
46 45 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. h e. J ( S C_ h /\ h C_ N ) ) ) )
47 38 44 46 3imtr4d 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( A. p e. S N e. ( ( nei ` J ) ` { p } ) -> N e. ( ( nei ` J ) ` S ) ) )
48 7 47 impbid 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( N e. ( ( nei ` J ) ` S ) <-> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )