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

Theorem neifil 17407
 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
StepHypRef Expression
1 toponuni 16497 . . . . . . . 8 TopOn
21adantr 453 . . . . . . 7 TopOn
3 topontop 16496 . . . . . . . . 9 TopOn
43adantr 453 . . . . . . . 8 TopOn
5 simpr 449 . . . . . . . . 9 TopOn
65, 2sseqtrd 3135 . . . . . . . 8 TopOn
7 eqid 2253 . . . . . . . . 9
87neiuni 16691 . . . . . . . 8
94, 6, 8syl2anc 645 . . . . . . 7 TopOn
102, 9eqtrd 2285 . . . . . 6 TopOn
11 eqimss2 3152 . . . . . 6
1210, 11syl 17 . . . . 5 TopOn
13 sspwuni 3885 . . . . 5
1412, 13sylibr 205 . . . 4 TopOn
15143adant3 980 . . 3 TopOn
16 0nnei 16681 . . . . 5
173, 16sylan 459 . . . 4 TopOn
18173adant2 979 . . 3 TopOn
197tpnei 16690 . . . . . . 7
2019biimpa 472 . . . . . 6
214, 6, 20syl2anc 645 . . . . 5 TopOn
222, 21eqeltrd 2327 . . . 4 TopOn
23223adant3 980 . . 3 TopOn
2415, 18, 233jca 1137 . 2 TopOn
25 elpwi 3538 . . . . 5
264ad2antrr 709 . . . . . . . 8 TopOn
27 simprl 735 . . . . . . . 8 TopOn
28 simprr 736 . . . . . . . 8 TopOn
29 simplr 734 . . . . . . . . 9 TopOn
302ad2antrr 709 . . . . . . . . 9 TopOn
3129, 30sseqtrd 3135 . . . . . . . 8 TopOn
327ssnei2 16685 . . . . . . . 8
3326, 27, 28, 31, 32syl22anc 1188 . . . . . . 7 TopOn
3433expr 601 . . . . . 6 TopOn
3534rexlimdva 2629 . . . . 5 TopOn
3625, 35sylan2 462 . . . 4 TopOn
3736ralrimiva 2588 . . 3 TopOn