Metamath Proof Explorer

Theorem gneispaceel2

Description: Every neighborhood of a point in a generic neighborhood space contains 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 gneispaceel2 
|- ( ( F e. A /\ P e. dom F /\ N e. ( F ` P ) ) -> P e. N )

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 gneispaceel 
 |-  ( F e. A -> A. p e. dom F A. n e. ( F ` p ) p e. n )
3 fveq2 
 |-  ( p = P -> ( F ` p ) = ( F ` P ) )
4 eleq1 
 |-  ( p = P -> ( p e. n <-> P e. n ) )
5 3 4 raleqbidv 
 |-  ( p = P -> ( A. n e. ( F ` p ) p e. n <-> A. n e. ( F ` P ) P e. n ) )
6 5 rspccv 
 |-  ( A. p e. dom F A. n e. ( F ` p ) p e. n -> ( P e. dom F -> A. n e. ( F ` P ) P e. n ) )
7 2 6 syl 
 |-  ( F e. A -> ( P e. dom F -> A. n e. ( F ` P ) P e. n ) )
8 eleq2 
 |-  ( n = N -> ( P e. n <-> P e. N ) )
9 8 rspccv 
 |-  ( A. n e. ( F ` P ) P e. n -> ( N e. ( F ` P ) -> P e. N ) )
10 7 9 syl6 
 |-  ( F e. A -> ( P e. dom F -> ( N e. ( F ` P ) -> P e. N ) ) )
11 10 3imp 
 |-  ( ( F e. A /\ P e. dom F /\ N e. ( F ` P ) ) -> P e. N )