Theorem gneispace2

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

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		id	|- ( f = F -> f = F )
3		dmeq	|- ( f = F -> dom f = dom F )
4	3	pweqd	|- ( f = F -> ~P dom f = ~P dom F )
5	4	difeq1d	|- ( f = F -> ( ~P dom f \ { (/) } ) = ( ~P dom F \ { (/) } ) )
6	5	pweqd	|- ( f = F -> ~P ( ~P dom f \ { (/) } ) = ~P ( ~P dom F \ { (/) } ) )
7	6	difeq1d	|- ( f = F -> ( ~P ( ~P dom f \ { (/) } ) \ { (/) } ) = ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
8	2 3 7	feq123d	|- ( f = F -> ( f : dom f --> ( ~P ( ~P dom f \ { (/) } ) \ { (/) } ) <-> F : dom F --> ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
9		fveq1	|- ( f = F -> ( f ` p ) = ( F ` p ) )
10	9	eleq2d	|- ( f = F -> ( s e. ( f ` p ) <-> s e. ( F ` p ) ) )
11	10	imbi2d	|- ( f = F -> ( ( n C_ s -> s e. ( f ` p ) ) <-> ( n C_ s -> s e. ( F ` p ) ) ) )
12	4 11	raleqbidv	|- ( f = F -> ( 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 ) ) ) )
13	12	anbi2d	|- ( f = F -> ( ( p e. n /\ A. s e. ~P dom f ( n C_ s -> s e. ( f ` p ) ) ) <-> ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) )
14	9 13	raleqbidv	|- ( f = F -> ( A. n e. ( f ` p ) ( p e. n /\ A. s e. ~P dom f ( n C_ s -> s e. ( f ` p ) ) ) <-> A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) )
15	3 14	raleqbidv	|- ( f = 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 ) ) ) <-> 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 ) ) ) ) )
16	8 15	anbi12d	|- ( f = 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 ) ) ) ) <-> ( 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 ) ) ) ) ) )
17	16 1	elab2g	|- ( 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 ) ) ) ) ) )