Metamath Proof Explorer

Theorem neibastop3

Description: The topology generated by a neighborhood base is unique. (Contributed by Jeff Hankins, 16-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 neibastop3 
|- ( ph -> E! j e. ( TopOn ` X ) A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) 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 1 2 3 4 5 6 neibastop2 
 |-  ( ( ph /\ z e. X ) -> ( n e. ( ( nei ` J ) ` { z } ) <-> ( n C_ X /\ ( ( F ` z ) i^i ~P n ) =/= (/) ) ) )
9 velpw 
 |-  ( n e. ~P X <-> n C_ X )
10 9 anbi1i 
 |-  ( ( n e. ~P X /\ ( ( F ` z ) i^i ~P n ) =/= (/) ) <-> ( n C_ X /\ ( ( F ` z ) i^i ~P n ) =/= (/) ) )
11 8 10 bitr4di 
 |-  ( ( ph /\ z e. X ) -> ( n e. ( ( nei ` J ) ` { z } ) <-> ( n e. ~P X /\ ( ( F ` z ) i^i ~P n ) =/= (/) ) ) )
12 11 eqabdv 
 |-  ( ( ph /\ z e. X ) -> ( ( nei ` J ) ` { z } ) = { n | ( n e. ~P X /\ ( ( F ` z ) i^i ~P n ) =/= (/) ) } )
13 df-rab 
 |-  { n e. ~P X | ( ( F ` z ) i^i ~P n ) =/= (/) } = { n | ( n e. ~P X /\ ( ( F ` z ) i^i ~P n ) =/= (/) ) }
14 12 13 eqtr4di 
 |-  ( ( ph /\ z e. X ) -> ( ( nei ` J ) ` { z } ) = { n e. ~P X | ( ( F ` z ) i^i ~P n ) =/= (/) } )
15 14 ralrimiva 
 |-  ( ph -> A. z e. X ( ( nei ` J ) ` { z } ) = { n e. ~P X | ( ( F ` z ) i^i ~P n ) =/= (/) } )
16 sneq 
 |-  ( x = z -> { x } = { z } )
17 16 fveq2d 
 |-  ( x = z -> ( ( nei ` J ) ` { x } ) = ( ( nei ` J ) ` { z } ) )
18 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
19 18 ineq1d 
 |-  ( x = z -> ( ( F ` x ) i^i ~P n ) = ( ( F ` z ) i^i ~P n ) )
20 19 neeq1d 
 |-  ( x = z -> ( ( ( F ` x ) i^i ~P n ) =/= (/) <-> ( ( F ` z ) i^i ~P n ) =/= (/) ) )
21 20 rabbidv 
 |-  ( x = z -> { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } = { n e. ~P X | ( ( F ` z ) i^i ~P n ) =/= (/) } )
22 17 21 eqeq12d 
 |-  ( x = z -> ( ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> ( ( nei ` J ) ` { z } ) = { n e. ~P X | ( ( F ` z ) i^i ~P n ) =/= (/) } ) )
23 22 cbvralvw 
 |-  ( A. x e. X ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> A. z e. X ( ( nei ` J ) ` { z } ) = { n e. ~P X | ( ( F ` z ) i^i ~P n ) =/= (/) } )
24 15 23 sylibr 
 |-  ( ph -> A. x e. X ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } )
25 toponuni 
 |-  ( j e. ( TopOn ` X ) -> X = U. j )
26 eqimss2 
 |-  ( X = U. j -> U. j C_ X )
27 25 26 syl 
 |-  ( j e. ( TopOn ` X ) -> U. j C_ X )
28 sspwuni 
 |-  ( j C_ ~P X <-> U. j C_ X )
29 27 28 sylibr 
 |-  ( j e. ( TopOn ` X ) -> j C_ ~P X )
30 29 ad2antlr 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> j C_ ~P X )
31 sseqin2 
 |-  ( j C_ ~P X <-> ( ~P X i^i j ) = j )
32 30 31 sylib 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> ( ~P X i^i j ) = j )
33 topontop 
 |-  ( j e. ( TopOn ` X ) -> j e. Top )
34 33 ad3antlr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) /\ o e. ~P X ) -> j e. Top )
35 eltop2 
 |-  ( j e. Top -> ( o e. j <-> A. x e. o E. z e. j ( x e. z /\ z C_ o ) ) )
36 34 35 syl 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) /\ o e. ~P X ) -> ( o e. j <-> A. x e. o E. z e. j ( x e. z /\ z C_ o ) ) )
37 elpwi 
 |-  ( o e. ~P X -> o C_ X )
38 ssralv 
 |-  ( o C_ X -> ( A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } -> A. x e. o ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
39 37 38 syl 
 |-  ( o e. ~P X -> ( A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } -> A. x e. o ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
40 39 adantl 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) -> ( A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } -> A. x e. o ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
41 simprr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } )
42 41 eleq2d 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> ( o e. ( ( nei ` j ) ` { x } ) <-> o e. { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
43 33 ad3antlr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> j e. Top )
44 25 adantl 
 |-  ( ( ph /\ j e. ( TopOn ` X ) ) -> X = U. j )
45 44 sseq2d 
 |-  ( ( ph /\ j e. ( TopOn ` X ) ) -> ( o C_ X <-> o C_ U. j ) )
46 45 biimpa 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o C_ X ) -> o C_ U. j )
47 37 46 sylan2 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) -> o C_ U. j )
48 47 sselda 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ x e. o ) -> x e. U. j )
49 48 adantrr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> x e. U. j )
50 47 adantr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> o C_ U. j )
51 eqid 
 |-  U. j = U. j
52 51 isneip 
 |-  ( ( j e. Top /\ x e. U. j ) -> ( o e. ( ( nei ` j ) ` { x } ) <-> ( o C_ U. j /\ E. z e. j ( x e. z /\ z C_ o ) ) ) )
53 52 baibd 
 |-  ( ( ( j e. Top /\ x e. U. j ) /\ o C_ U. j ) -> ( o e. ( ( nei ` j ) ` { x } ) <-> E. z e. j ( x e. z /\ z C_ o ) ) )
54 43 49 50 53 syl21anc 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> ( o e. ( ( nei ` j ) ` { x } ) <-> E. z e. j ( x e. z /\ z C_ o ) ) )
55 pweq 
 |-  ( n = o -> ~P n = ~P o )
56 55 ineq2d 
 |-  ( n = o -> ( ( F ` x ) i^i ~P n ) = ( ( F ` x ) i^i ~P o ) )
57 56 neeq1d 
 |-  ( n = o -> ( ( ( F ` x ) i^i ~P n ) =/= (/) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) )
58 57 elrab3 
 |-  ( o e. ~P X -> ( o e. { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) )
59 58 ad2antlr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> ( o e. { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) )
60 42 54 59 3bitr3d 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ ( x e. o /\ ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) -> ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) )
61 60 expr 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ x e. o ) -> ( ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } -> ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) ) )
62 61 ralimdva 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) -> ( A. x e. o ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } -> A. x e. o ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) ) )
63 40 62 syld 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) -> ( A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } -> A. x e. o ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) ) )
64 63 imp 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ o e. ~P X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> A. x e. o ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) )
65 64 an32s 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) /\ o e. ~P X ) -> A. x e. o ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) )
66 ralbi 
 |-  ( A. x e. o ( E. z e. j ( x e. z /\ z C_ o ) <-> ( ( F ` x ) i^i ~P o ) =/= (/) ) -> ( A. x e. o E. z e. j ( x e. z /\ z C_ o ) <-> A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) ) )
67 65 66 syl 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) /\ o e. ~P X ) -> ( A. x e. o E. z e. j ( x e. z /\ z C_ o ) <-> A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) ) )
68 36 67 bitrd 
 |-  ( ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) /\ o e. ~P X ) -> ( o e. j <-> A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) ) )
69 68 rabbi2dva 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> ( ~P X i^i j ) = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) } )
70 69 4 eqtr4di 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> ( ~P X i^i j ) = J )
71 32 70 eqtr3d 
 |-  ( ( ( ph /\ j e. ( TopOn ` X ) ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> j = J )
72 71 expl 
 |-  ( ph -> ( ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> j = J ) )
73 72 alrimiv 
 |-  ( ph -> A. j ( ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> j = J ) )
74 eleq1 
 |-  ( j = J -> ( j e. ( TopOn ` X ) <-> J e. ( TopOn ` X ) ) )
75 fveq2 
 |-  ( j = J -> ( nei ` j ) = ( nei ` J ) )
76 75 fveq1d 
 |-  ( j = J -> ( ( nei ` j ) ` { x } ) = ( ( nei ` J ) ` { x } ) )
77 76 eqeq1d 
 |-  ( j = J -> ( ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
78 77 ralbidv 
 |-  ( j = J -> ( A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> A. x e. X ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
79 74 78 anbi12d 
 |-  ( j = J -> ( ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) <-> ( J e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) ) )
80 79 eqeu 
 |-  ( ( J e. ( TopOn ` X ) /\ ( J e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` J ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) /\ A. j ( ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) -> j = J ) ) -> E! j ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
81 7 7 24 73 80 syl121anc 
 |-  ( ph -> E! j ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
82 df-reu 
 |-  ( E! j e. ( TopOn ` X ) A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } <-> E! j ( j e. ( TopOn ` X ) /\ A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } ) )
83 81 82 sylibr 
 |-  ( ph -> E! j e. ( TopOn ` X ) A. x e. X ( ( nei ` j ) ` { x } ) = { n e. ~P X | ( ( F ` x ) i^i ~P n ) =/= (/) } )