Theorem gneispacess

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	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 ) ) )

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		simpr	|- ( ( p e. 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 ) ) )
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 ) A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) )
6	3 5	simpl2im	|- ( 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 ) ) )