Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neifil Structured version   Unicode version

Theorem neifil 20675
 Description: The neighborhoods of a nonempty set is a filter. Example 2 of [BourbakiTop1] p. I.36. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
Assertion
Ref Expression
neifil TopOn

Proof of Theorem neifil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 toponuni 19722 . . . . . . . 8 TopOn
21adantr 465 . . . . . . 7 TopOn
3 topontop 19721 . . . . . . . . 9 TopOn
43adantr 465 . . . . . . . 8 TopOn
5 simpr 461 . . . . . . . . 9 TopOn
65, 2sseqtrd 3480 . . . . . . . 8 TopOn
7 eqid 2404 . . . . . . . . 9
87neiuni 19918 . . . . . . . 8
94, 6, 8syl2anc 661 . . . . . . 7 TopOn
102, 9eqtrd 2445 . . . . . 6 TopOn
11 eqimss2 3497 . . . . . 6
1210, 11syl 17 . . . . 5 TopOn
13 sspwuni 4362 . . . . 5
1412, 13sylibr 214 . . . 4 TopOn
15143adant3 1019 . . 3 TopOn
16 0nnei 19908 . . . . 5
173, 16sylan 471 . . . 4 TopOn
18173adant2 1018 . . 3 TopOn
197tpnei 19917 . . . . . . 7
2019biimpa 484 . . . . . 6
214, 6, 20syl2anc 661 . . . . 5 TopOn
222, 21eqeltrd 2492 . . . 4 TopOn
23223adant3 1019 . . 3 TopOn
2415, 18, 233jca 1179 . 2 TopOn
25 elpwi 3966 . . . . 5
264ad2antrr 726 . . . . . . 7 TopOn
27 simprl 758 . . . . . . 7 TopOn
28 simprr 760 . . . . . . 7 TopOn
29 simplr 756 . . . . . . . 8 TopOn
302ad2antrr 726 . . . . . . . 8 TopOn
3129, 30sseqtrd 3480 . . . . . . 7 TopOn
327ssnei2 19912 . . . . . . 7
3326, 27, 28, 31, 32syl22anc 1233 . . . . . 6 TopOn
3433rexlimdvaa 2899 . . . . 5 TopOn
3525, 34sylan2 474 . . . 4 TopOn
3635ralrimiva 2820 . . 3 TopOn