Theorem gneispace0nelrn3

Description: A generic neighborhood space has a nonempty set of neighborhoods for every point in its domain. (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	gneispace0nelrn3	|- ( F e. A -> -. (/) e. ran F )

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	gneispacern	|- ( F e. A -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
3		neldifsnd	|- ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) -> -. (/) e. ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
4		ssel	|- ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) -> ( (/) e. ran F -> (/) e. ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
5	3 4	mtod	|- ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) -> -. (/) e. ran F )
6	2 5	syl	|- ( F e. A -> -. (/) e. ran F )