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

Theorem neifil 17575
 Description: The neighborhoods of a non empty 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 16665 . . . . . . . 8 TopOn
21adantr 451 . . . . . . 7 TopOn
3 topontop 16664 . . . . . . . . 9 TopOn
43adantr 451 . . . . . . . 8 TopOn
5 simpr 447 . . . . . . . . 9 TopOn
65, 2sseqtrd 3214 . . . . . . . 8 TopOn
7 eqid 2283 . . . . . . . . 9
87neiuni 16859 . . . . . . . 8
94, 6, 8syl2anc 642 . . . . . . 7 TopOn
102, 9eqtrd 2315 . . . . . 6 TopOn
11 eqimss2 3231 . . . . . 6
1210, 11syl 15 . . . . 5 TopOn
13 sspwuni 3987 . . . . 5
1412, 13sylibr 203 . . . 4 TopOn
15143adant3 975 . . 3 TopOn
16 0nnei 16849 . . . . 5
173, 16sylan 457 . . . 4 TopOn
18173adant2 974 . . 3 TopOn
197tpnei 16858 . . . . . . 7
2019biimpa 470 . . . . . 6
214, 6, 20syl2anc 642 . . . . 5 TopOn
222, 21eqeltrd 2357 . . . 4 TopOn
23223adant3 975 . . 3 TopOn
2415, 18, 233jca 1132 . 2 TopOn
25 elpwi 3633 . . . . 5
264ad2antrr 706 . . . . . . . 8 TopOn
27 simprl 732 . . . . . . . 8 TopOn
28 simprr 733 . . . . . . . 8 TopOn
29 simplr 731 . . . . . . . . 9 TopOn
302ad2antrr 706 . . . . . . . . 9 TopOn
3129, 30sseqtrd 3214 . . . . . . . 8 TopOn
327ssnei2 16853 . . . . . . . 8
3326, 27, 28, 31, 32syl22anc 1183 . . . . . . 7 TopOn
3433expr 598 . . . . . 6 TopOn
3534rexlimdva 2667 . . . . 5 TopOn
3625, 35sylan2 460 . . . 4 TopOn
3736ralrimiva 2626 . . 3 TopOn