Metamath Proof Explorer

Theorem gneispacern2

Description: A generic neighborhood space has a range that is a subset of the powerset of the powerset of 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 gneispacern2 
|- ( F e. A -> ran F C_ ~P ~P dom 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 elex 
 |-  ( F e. A -> F e. _V )
3 1 gneispace 
 |-  ( F e. _V -> ( F e. A <-> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) ) )
4 2 3 syl 
 |-  ( F e. A -> ( F e. A <-> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) ) )
5 4 ibi 
 |-  ( F e. A -> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) )
6 5 simp2d 
 |-  ( F e. A -> ran F C_ ~P ~P dom F )