Metamath Proof Explorer

Theorem gneispacess2

Description: All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021)

Ref Expression
Hypothesis gneispace.a 
|- A = { f | ( f : dom f --> ( ~P ( ~P dom f \ { (/) } ) \ { (/) } ) /\ A. p e. dom f A. n e. ( f ` p ) ( p e. n /\ A. s e. ~P dom f ( n C_ s -> s e. ( f ` p ) ) ) ) }
Assertion gneispacess2 
|- ( ( ( F e. A /\ P e. dom F ) /\ ( N e. ( F ` P ) /\ S e. ~P dom F /\ N C_ S ) ) -> S e. ( F ` P ) )

Proof

Step Hyp Ref Expression
1 gneispace.a 
 |-  A = { f | ( f : dom f --> ( ~P ( ~P dom f \ { (/) } ) \ { (/) } ) /\ A. p e. dom f A. n e. ( f ` p ) ( p e. n /\ A. s e. ~P dom f ( n C_ s -> s e. ( f ` p ) ) ) ) }
2 1 gneispacess 
 |-  ( F e. A -> A. p e. dom F A. n e. ( F ` p ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) )
3 fveq2 
 |-  ( p = P -> ( F ` p ) = ( F ` P ) )
4 3 eleq2d 
 |-  ( p = P -> ( s e. ( F ` p ) <-> s e. ( F ` P ) ) )
5 4 imbi2d 
 |-  ( p = P -> ( ( n C_ s -> s e. ( F ` p ) ) <-> ( n C_ s -> s e. ( F ` P ) ) ) )
6 5 ralbidv 
 |-  ( p = P -> ( A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) <-> A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) ) )
7 3 6 raleqbidv 
 |-  ( p = P -> ( A. n e. ( F ` p ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) <-> A. n e. ( F ` P ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) ) )
8 7 rspccv 
 |-  ( A. p e. dom F A. n e. ( F ` p ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) -> ( P e. dom F -> A. n e. ( F ` P ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) ) )
9 2 8 syl 
 |-  ( F e. A -> ( P e. dom F -> A. n e. ( F ` P ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) ) )
10 sseq1 
 |-  ( n = N -> ( n C_ s <-> N C_ s ) )
11 10 imbi1d 
 |-  ( n = N -> ( ( n C_ s -> s e. ( F ` P ) ) <-> ( N C_ s -> s e. ( F ` P ) ) ) )
12 11 ralbidv 
 |-  ( n = N -> ( A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) <-> A. s e. ~P dom F ( N C_ s -> s e. ( F ` P ) ) ) )
13 12 rspccv 
 |-  ( A. n e. ( F ` P ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) -> ( N e. ( F ` P ) -> A. s e. ~P dom F ( N C_ s -> s e. ( F ` P ) ) ) )
14 sseq2 
 |-  ( s = S -> ( N C_ s <-> N C_ S ) )
15 eleq1 
 |-  ( s = S -> ( s e. ( F ` P ) <-> S e. ( F ` P ) ) )
16 14 15 imbi12d 
 |-  ( s = S -> ( ( N C_ s -> s e. ( F ` P ) ) <-> ( N C_ S -> S e. ( F ` P ) ) ) )
17 16 rspccv 
 |-  ( A. s e. ~P dom F ( N C_ s -> s e. ( F ` P ) ) -> ( S e. ~P dom F -> ( N C_ S -> S e. ( F ` P ) ) ) )
18 13 17 syl6 
 |-  ( A. n e. ( F ` P ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) -> ( N e. ( F ` P ) -> ( S e. ~P dom F -> ( N C_ S -> S e. ( F ` P ) ) ) ) )
19 18 3impd 
 |-  ( A. n e. ( F ` P ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` P ) ) -> ( ( N e. ( F ` P ) /\ S e. ~P dom F /\ N C_ S ) -> S e. ( F ` P ) ) )
20 9 19 syl6 
 |-  ( F e. A -> ( P e. dom F -> ( ( N e. ( F ` P ) /\ S e. ~P dom F /\ N C_ S ) -> S e. ( F ` P ) ) ) )
21 20 imp31 
 |-  ( ( ( F e. A /\ P e. dom F ) /\ ( N e. ( F ` P ) /\ S e. ~P dom F /\ N C_ S ) ) -> S e. ( F ` P ) )