Metamath Proof Explorer

Theorem gneispace3

Description: The predicate that F is a (generic) Seifert and Threlfall neighborhood space. (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 gneispace3 
|- ( F e. V -> ( F e. A <-> ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) ) )

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. V -> ( 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 df-f 
 |-  ( F : dom F --> ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) <-> ( F Fn dom F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
4 funfn 
 |-  ( Fun F <-> F Fn dom F )
5 4 anbi1i 
 |-  ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) <-> ( F Fn dom F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
6 3 5 bitr4i 
 |-  ( F : dom F --> ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) <-> ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
7 6 anbi1i 
 |-  ( ( 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 ) ) ) ) <-> ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) )
8 2 7 bitrdi 
 |-  ( F e. V -> ( F e. A <-> ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) ) )