Metamath Proof Explorer

Theorem neibastop2

Description: In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses neibastop1.1 
|- ( ph -> X e. V )
neibastop1.2 
|- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )
neibastop1.3 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
neibastop1.4 
|- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }
neibastop1.5 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )
neibastop1.6 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
Assertion neibastop2 
|- ( ( ph /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 neibastop1.1 
 |-  ( ph -> X e. V )
2 neibastop1.2 
 |-  ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )
3 neibastop1.3 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
4 neibastop1.4 
 |-  J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }
5 neibastop1.5 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )
6 neibastop1.6 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
7 1 2 3 4 neibastop1 
 |-  ( ph -> J e. ( TopOn ` X ) )
8 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
9 7 8 syl 
 |-  ( ph -> J e. Top )
10 9 adantr 
 |-  ( ( ph /\ P e. X ) -> J e. Top )
11 eqid 
 |-  U. J = U. J
12 11 neii1 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` { P } ) ) -> N C_ U. J )
13 10 12 sylan 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> N C_ U. J )
14 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
15 7 14 syl 
 |-  ( ph -> X = U. J )
16 15 ad2antrr 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> X = U. J )
17 13 16 sseqtrrd 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> N C_ X )
18 neii2 
 |-  ( ( J e. Top /\ N e. ( ( nei ` J ) ` { P } ) ) -> E. y e. J ( { P } C_ y /\ y C_ N ) )
19 10 18 sylan 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> E. y e. J ( { P } C_ y /\ y C_ N ) )
20 pweq 
 |-  ( o = y -> ~P o = ~P y )
21 20 ineq2d 
 |-  ( o = y -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P y ) )
22 21 neeq1d 
 |-  ( o = y -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P y ) =/= (/) ) )
23 22 raleqbi1dv 
 |-  ( o = y -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) )
24 23 4 elrab2 
 |-  ( y e. J <-> ( y e. ~P X /\ A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) )
25 simprrr 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> y C_ N )
26 25 sspwd 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> ~P y C_ ~P N )
27 sslin 
 |-  ( ~P y C_ ~P N -> ( ( F ` P ) i^i ~P y ) C_ ( ( F ` P ) i^i ~P N ) )
28 26 27 syl 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> ( ( F ` P ) i^i ~P y ) C_ ( ( F ` P ) i^i ~P N ) )
29 simprrl 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> { P } C_ y )
30 snssg 
 |-  ( P e. X -> ( P e. y <-> { P } C_ y ) )
31 30 ad3antlr 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> ( P e. y <-> { P } C_ y ) )
32 29 31 mpbird 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> P e. y )
33 fveq2 
 |-  ( x = P -> ( F ` x ) = ( F ` P ) )
34 33 ineq1d 
 |-  ( x = P -> ( ( F ` x ) i^i ~P y ) = ( ( F ` P ) i^i ~P y ) )
35 34 neeq1d 
 |-  ( x = P -> ( ( ( F ` x ) i^i ~P y ) =/= (/) <-> ( ( F ` P ) i^i ~P y ) =/= (/) ) )
36 35 rspcv 
 |-  ( P e. y -> ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> ( ( F ` P ) i^i ~P y ) =/= (/) ) )
37 32 36 syl 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> ( ( F ` P ) i^i ~P y ) =/= (/) ) )
38 ssn0 
 |-  ( ( ( ( F ` P ) i^i ~P y ) C_ ( ( F ` P ) i^i ~P N ) /\ ( ( F ` P ) i^i ~P y ) =/= (/) ) -> ( ( F ` P ) i^i ~P N ) =/= (/) )
39 28 37 38 syl6an 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ ( y e. ~P X /\ ( { P } C_ y /\ y C_ N ) ) ) -> ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> ( ( F ` P ) i^i ~P N ) =/= (/) ) )
40 39 expr 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ y e. ~P X ) -> ( ( { P } C_ y /\ y C_ N ) -> ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )
41 40 com23 
 |-  ( ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) /\ y e. ~P X ) -> ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> ( ( { P } C_ y /\ y C_ N ) -> ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )
42 41 expimpd 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( ( y e. ~P X /\ A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) -> ( ( { P } C_ y /\ y C_ N ) -> ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )
43 24 42 biimtrid 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( y e. J -> ( ( { P } C_ y /\ y C_ N ) -> ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )
44 43 rexlimdv 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( E. y e. J ( { P } C_ y /\ y C_ N ) -> ( ( F ` P ) i^i ~P N ) =/= (/) ) )
45 19 44 mpd 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( ( F ` P ) i^i ~P N ) =/= (/) )
46 17 45 jca 
 |-  ( ( ( ph /\ P e. X ) /\ N e. ( ( nei ` J ) ` { P } ) ) -> ( N C_ X /\ ( ( F ` P ) i^i ~P N ) =/= (/) ) )
47 46 ex 
 |-  ( ( ph /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) -> ( N C_ X /\ ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )
48 n0 
 |-  ( ( ( F ` P ) i^i ~P N ) =/= (/) <-> E. s s e. ( ( F ` P ) i^i ~P N ) )
49 elin 
 |-  ( s e. ( ( F ` P ) i^i ~P N ) <-> ( s e. ( F ` P ) /\ s e. ~P N ) )
50 simprl 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> N C_ X )
51 15 ad2antrr 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> X = U. J )
52 50 51 sseqtrd 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> N C_ U. J )
53 1 ad2antrr 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> X e. V )
54 2 ad2antrr 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> F : X --> ( ~P ~P X \ { (/) } ) )
55 simpll 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> ph )
56 55 3 sylan 
 |-  ( ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
57 55 5 sylan 
 |-  ( ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) /\ ( x e. X /\ v e. ( F ` x ) ) ) -> x e. v )
58 55 6 sylan 
 |-  ( ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) /\ ( x e. X /\ v e. ( F ` x ) ) ) -> E. t e. ( F ` x ) A. y e. t ( ( F ` y ) i^i ~P v ) =/= (/) )
59 simplr 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> P e. X )
60 simprrl 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> s e. ( F ` P ) )
61 simprrr 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> s e. ~P N )
62 61 elpwid 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> s C_ N )
63 fveq2 
 |-  ( n = x -> ( F ` n ) = ( F ` x ) )
64 63 ineq1d 
 |-  ( n = x -> ( ( F ` n ) i^i ~P b ) = ( ( F ` x ) i^i ~P b ) )
65 64 cbviunv 
 |-  U_ n e. X ( ( F ` n ) i^i ~P b ) = U_ x e. X ( ( F ` x ) i^i ~P b )
66 pweq 
 |-  ( b = z -> ~P b = ~P z )
67 66 ineq2d 
 |-  ( b = z -> ( ( F ` x ) i^i ~P b ) = ( ( F ` x ) i^i ~P z ) )
68 67 iuneq2d 
 |-  ( b = z -> U_ x e. X ( ( F ` x ) i^i ~P b ) = U_ x e. X ( ( F ` x ) i^i ~P z ) )
69 65 68 eqtrid 
 |-  ( b = z -> U_ n e. X ( ( F ` n ) i^i ~P b ) = U_ x e. X ( ( F ` x ) i^i ~P z ) )
70 69 cbviunv 
 |-  U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) = U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z )
71 70 mpteq2i 
 |-  ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) = ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) )
72 rdgeq1 
 |-  ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) = ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) -> rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) = rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { s } ) )
73 71 72 ax-mp 
 |-  rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) = rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { s } )
74 73 reseq1i 
 |-  ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) = ( rec ( ( a e. _V |-> U_ z e. a U_ x e. X ( ( F ` x ) i^i ~P z ) ) , { s } ) |` _om )
75 pweq 
 |-  ( g = f -> ~P g = ~P f )
76 75 ineq2d 
 |-  ( g = f -> ( ( F ` w ) i^i ~P g ) = ( ( F ` w ) i^i ~P f ) )
77 76 neeq1d 
 |-  ( g = f -> ( ( ( F ` w ) i^i ~P g ) =/= (/) <-> ( ( F ` w ) i^i ~P f ) =/= (/) ) )
78 77 cbvrexvw 
 |-  ( E. g e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` w ) i^i ~P g ) =/= (/) <-> E. f e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` w ) i^i ~P f ) =/= (/) )
79 fveq2 
 |-  ( w = y -> ( F ` w ) = ( F ` y ) )
80 79 ineq1d 
 |-  ( w = y -> ( ( F ` w ) i^i ~P f ) = ( ( F ` y ) i^i ~P f ) )
81 80 neeq1d 
 |-  ( w = y -> ( ( ( F ` w ) i^i ~P f ) =/= (/) <-> ( ( F ` y ) i^i ~P f ) =/= (/) ) )
82 81 rexbidv 
 |-  ( w = y -> ( E. f e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` w ) i^i ~P f ) =/= (/) <-> E. f e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` y ) i^i ~P f ) =/= (/) ) )
83 78 82 bitrid 
 |-  ( w = y -> ( E. g e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` w ) i^i ~P g ) =/= (/) <-> E. f e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` y ) i^i ~P f ) =/= (/) ) )
84 83 cbvrabv 
 |-  { w e. X | E. g e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` w ) i^i ~P g ) =/= (/) } = { y e. X | E. f e. U. ran ( rec ( ( a e. _V |-> U_ b e. a U_ n e. X ( ( F ` n ) i^i ~P b ) ) , { s } ) |` _om ) ( ( F ` y ) i^i ~P f ) =/= (/) }
85 53 54 56 4 57 58 59 50 60 62 74 84 neibastop2lem 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> E. u e. J ( P e. u /\ u C_ N ) )
86 9 ad2antrr 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> J e. Top )
87 59 51 eleqtrd 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> P e. U. J )
88 11 isneip 
 |-  ( ( J e. Top /\ P e. U. J ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ U. J /\ E. u e. J ( P e. u /\ u C_ N ) ) ) )
89 86 87 88 syl2anc 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ U. J /\ E. u e. J ( P e. u /\ u C_ N ) ) ) )
90 52 85 89 mpbir2and 
 |-  ( ( ( ph /\ P e. X ) /\ ( N C_ X /\ ( s e. ( F ` P ) /\ s e. ~P N ) ) ) -> N e. ( ( nei ` J ) ` { P } ) )
91 90 expr 
 |-  ( ( ( ph /\ P e. X ) /\ N C_ X ) -> ( ( s e. ( F ` P ) /\ s e. ~P N ) -> N e. ( ( nei ` J ) ` { P } ) ) )
92 49 91 biimtrid 
 |-  ( ( ( ph /\ P e. X ) /\ N C_ X ) -> ( s e. ( ( F ` P ) i^i ~P N ) -> N e. ( ( nei ` J ) ` { P } ) ) )
93 92 exlimdv 
 |-  ( ( ( ph /\ P e. X ) /\ N C_ X ) -> ( E. s s e. ( ( F ` P ) i^i ~P N ) -> N e. ( ( nei ` J ) ` { P } ) ) )
94 48 93 biimtrid 
 |-  ( ( ( ph /\ P e. X ) /\ N C_ X ) -> ( ( ( F ` P ) i^i ~P N ) =/= (/) -> N e. ( ( nei ` J ) ` { P } ) ) )
95 94 expimpd 
 |-  ( ( ph /\ P e. X ) -> ( ( N C_ X /\ ( ( F ` P ) i^i ~P N ) =/= (/) ) -> N e. ( ( nei ` J ) ` { P } ) ) )
96 47 95 impbid 
 |-  ( ( ph /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ ( ( F ` P ) i^i ~P N ) =/= (/) ) ) )