Metamath Proof Explorer

Theorem gneispace0nelrn2

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 gneispace0nelrn2 
|- ( ( F e. A /\ P e. dom F ) -> ( 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 gneispace0nelrn 
 |-  ( F e. A -> A. p e. dom F ( F ` p ) =/= (/) )
3 fveq2 
 |-  ( p = P -> ( F ` p ) = ( F ` P ) )
4 3 neeq1d 
 |-  ( p = P -> ( ( F ` p ) =/= (/) <-> ( F ` P ) =/= (/) ) )
5 4 rspccv 
 |-  ( A. p e. dom F ( F ` p ) =/= (/) -> ( P e. dom F -> ( F ` P ) =/= (/) ) )
6 2 5 syl 
 |-  ( F e. A -> ( P e. dom F -> ( F ` P ) =/= (/) ) )
7 6 imp 
 |-  ( ( F e. A /\ P e. dom F ) -> ( F ` P ) =/= (/) )