Metamath Proof Explorer


Theorem neibastop1

Description: A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard'sGeneral Topology. (Contributed by Jeff Hankins, 8-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses neibastop1.1 φXV
neibastop1.2 φF:X𝒫𝒫X
neibastop1.3 φxXvFxwFxFx𝒫vw
neibastop1.4 J=o𝒫X|xoFx𝒫o
Assertion neibastop1 φJTopOnX

Proof

Step Hyp Ref Expression
1 neibastop1.1 φXV
2 neibastop1.2 φF:X𝒫𝒫X
3 neibastop1.3 φxXvFxwFxFx𝒫vw
4 neibastop1.4 J=o𝒫X|xoFx𝒫o
5 simpr φyJyJ
6 ssrab2 o𝒫X|xoFx𝒫o𝒫X
7 4 6 eqsstri J𝒫X
8 5 7 sstrdi φyJy𝒫X
9 sspwuni y𝒫XyX
10 8 9 sylib φyJyX
11 vuniex yV
12 11 elpw y𝒫XyX
13 10 12 sylibr φyJy𝒫X
14 eluni2 xyzyxz
15 elssuni zyzy
16 15 ad2antrl φyJzyxzzy
17 16 sspwd φyJzyxz𝒫z𝒫y
18 sslin 𝒫z𝒫yFx𝒫zFx𝒫y
19 17 18 syl φyJzyxzFx𝒫zFx𝒫y
20 5 sselda φyJzyzJ
21 20 adantrr φyJzyxzzJ
22 pweq o=z𝒫o=𝒫z
23 22 ineq2d o=zFx𝒫o=Fx𝒫z
24 23 neeq1d o=zFx𝒫oFx𝒫z
25 24 raleqbi1dv o=zxoFx𝒫oxzFx𝒫z
26 25 4 elrab2 zJz𝒫XxzFx𝒫z
27 26 simprbi zJxzFx𝒫z
28 21 27 syl φyJzyxzxzFx𝒫z
29 simprr φyJzyxzxz
30 rsp xzFx𝒫zxzFx𝒫z
31 28 29 30 sylc φyJzyxzFx𝒫z
32 ssn0 Fx𝒫zFx𝒫yFx𝒫zFx𝒫y
33 19 31 32 syl2anc φyJzyxzFx𝒫y
34 33 rexlimdvaa φyJzyxzFx𝒫y
35 14 34 syl5bi φyJxyFx𝒫y
36 35 ralrimiv φyJxyFx𝒫y
37 pweq o=y𝒫o=𝒫y
38 37 ineq2d o=yFx𝒫o=Fx𝒫y
39 38 neeq1d o=yFx𝒫oFx𝒫y
40 39 raleqbi1dv o=yxoFx𝒫oxyFx𝒫y
41 40 4 elrab2 yJy𝒫XxyFx𝒫y
42 13 36 41 sylanbrc φyJyJ
43 42 ex φyJyJ
44 43 alrimiv φyyJyJ
45 pweq o=y𝒫o=𝒫y
46 45 ineq2d o=yFx𝒫o=Fx𝒫y
47 46 neeq1d o=yFx𝒫oFx𝒫y
48 47 raleqbi1dv o=yxoFx𝒫oxyFx𝒫y
49 48 4 elrab2 yJy𝒫XxyFx𝒫y
50 49 26 anbi12i yJzJy𝒫XxyFx𝒫yz𝒫XxzFx𝒫z
51 an4 y𝒫XxyFx𝒫yz𝒫XxzFx𝒫zy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫z
52 50 51 bitri yJzJy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫z
53 inss1 yzy
54 elpwi y𝒫XyX
55 53 54 sstrid y𝒫XyzX
56 55 ad2antrl φy𝒫Xz𝒫XyzX
57 56 adantrr φy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫zyzX
58 vex yV
59 58 inex1 yzV
60 59 elpw yz𝒫XyzX
61 57 60 sylibr φy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫zyz𝒫X
62 ssralv yzyxyFx𝒫yxyzFx𝒫y
63 53 62 ax-mp xyFx𝒫yxyzFx𝒫y
64 inss2 yzz
65 ssralv yzzxzFx𝒫zxyzFx𝒫z
66 64 65 ax-mp xzFx𝒫zxyzFx𝒫z
67 63 66 anim12i xyFx𝒫yxzFx𝒫zxyzFx𝒫yxyzFx𝒫z
68 r19.26 xyzFx𝒫yFx𝒫zxyzFx𝒫yxyzFx𝒫z
69 67 68 sylibr xyFx𝒫yxzFx𝒫zxyzFx𝒫yFx𝒫z
70 n0 Fx𝒫yvvFx𝒫y
71 n0 Fx𝒫zwwFx𝒫z
72 70 71 anbi12i Fx𝒫yFx𝒫zvvFx𝒫ywwFx𝒫z
73 exdistrv vwvFx𝒫ywFx𝒫zvvFx𝒫ywwFx𝒫z
74 inss2 Fx𝒫y𝒫y
75 simprl φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zvFx𝒫y
76 74 75 sselid φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zv𝒫y
77 76 elpwid φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zvy
78 inss2 Fx𝒫z𝒫z
79 simprr φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zwFx𝒫z
80 78 79 sselid φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zw𝒫z
81 80 elpwid φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zwz
82 ss2in vywzvwyz
83 77 81 82 syl2anc φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zvwyz
84 83 sspwd φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫z𝒫vw𝒫yz
85 sslin 𝒫vw𝒫yzFx𝒫vwFx𝒫yz
86 84 85 syl φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zFx𝒫vwFx𝒫yz
87 simplll φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zφ
88 56 ad2antrr φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zyzX
89 simplr φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zxyz
90 88 89 sseldd φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zxX
91 inss1 Fx𝒫yFx
92 91 75 sselid φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zvFx
93 inss1 Fx𝒫zFx
94 93 79 sselid φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zwFx
95 87 90 92 94 3 syl13anc φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zFx𝒫vw
96 ssn0 Fx𝒫vwFx𝒫yzFx𝒫vwFx𝒫yz
97 86 95 96 syl2anc φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zFx𝒫yz
98 97 ex φy𝒫Xz𝒫XxyzvFx𝒫ywFx𝒫zFx𝒫yz
99 98 exlimdvv φy𝒫Xz𝒫XxyzvwvFx𝒫ywFx𝒫zFx𝒫yz
100 73 99 syl5bir φy𝒫Xz𝒫XxyzvvFx𝒫ywwFx𝒫zFx𝒫yz
101 72 100 syl5bi φy𝒫Xz𝒫XxyzFx𝒫yFx𝒫zFx𝒫yz
102 101 ralimdva φy𝒫Xz𝒫XxyzFx𝒫yFx𝒫zxyzFx𝒫yz
103 69 102 syl5 φy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫zxyzFx𝒫yz
104 103 impr φy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫zxyzFx𝒫yz
105 pweq o=yz𝒫o=𝒫yz
106 105 ineq2d o=yzFx𝒫o=Fx𝒫yz
107 106 neeq1d o=yzFx𝒫oFx𝒫yz
108 107 raleqbi1dv o=yzxoFx𝒫oxyzFx𝒫yz
109 108 4 elrab2 yzJyz𝒫XxyzFx𝒫yz
110 61 104 109 sylanbrc φy𝒫Xz𝒫XxyFx𝒫yxzFx𝒫zyzJ
111 52 110 sylan2b φyJzJyzJ
112 111 ralrimivva φyJzJyzJ
113 sspwuni J𝒫XJX
114 7 113 mpbi JX
115 114 a1i φJX
116 1 115 ssexd φJV
117 uniexb JVJV
118 116 117 sylibr φJV
119 istopg JVJTopyyJyJyJzJyzJ
120 118 119 syl φJTopyyJyJyJzJyzJ
121 44 112 120 mpbir2and φJTop
122 pwidg XVX𝒫X
123 1 122 syl φX𝒫X
124 2 ffvelrnda φxXFx𝒫𝒫X
125 eldifi Fx𝒫𝒫XFx𝒫𝒫X
126 elpwi Fx𝒫𝒫XFx𝒫X
127 124 125 126 3syl φxXFx𝒫X
128 df-ss Fx𝒫XFx𝒫X=Fx
129 127 128 sylib φxXFx𝒫X=Fx
130 eldifsni Fx𝒫𝒫XFx
131 124 130 syl φxXFx
132 129 131 eqnetrd φxXFx𝒫X
133 132 ralrimiva φxXFx𝒫X
134 pweq o=X𝒫o=𝒫X
135 134 ineq2d o=XFx𝒫o=Fx𝒫X
136 135 neeq1d o=XFx𝒫oFx𝒫X
137 136 raleqbi1dv o=XxoFx𝒫oxXFx𝒫X
138 137 4 elrab2 XJX𝒫XxXFx𝒫X
139 123 133 138 sylanbrc φXJ
140 elssuni XJXJ
141 139 140 syl φXJ
142 141 115 eqssd φX=J
143 istopon JTopOnXJTopX=J
144 121 142 143 sylanbrc φJTopOnX