Metamath Proof Explorer


Theorem gneispaceel

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 gneispaceel
|- ( F e. A -> A. p e. dom F A. 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 gneispace2
 |-  ( F e. A -> ( F e. A <-> ( 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 ) ) ) ) ) )
3 2 ibi
 |-  ( F e. A -> ( 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 ) ) ) ) )
4 simpl
 |-  ( ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> p e. n )
5 4 2ralimi
 |-  ( 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 ) ) ) -> A. p e. dom F A. n e. ( F ` p ) p e. n )
6 3 5 simpl2im
 |-  ( F e. A -> A. p e. dom F A. n e. ( F ` p ) p e. n )