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

Theorem opnfbas 17866
 Description: The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.)
Hypothesis
Ref Expression
opnfbas.1
Assertion
Ref Expression
opnfbas
Distinct variable groups:   ,   ,   ,

Proof of Theorem opnfbas
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3420 . . . 4
2 opnfbas.1 . . . . . 6
32eqimss2i 3395 . . . . 5
4 sspwuni 4168 . . . . 5
53, 4mpbir 201 . . . 4
61, 5sstri 3349 . . 3
76a1i 11 . 2
82topopn 16971 . . . . . . 7
98anim1i 552 . . . . . 6
1093adant3 977 . . . . 5
11 sseq2 3362 . . . . . 6
1211elrab 3084 . . . . 5
1310, 12sylibr 204 . . . 4
14 ne0i 3626 . . . 4
1513, 14syl 16 . . 3
16 ss0 3650 . . . . . . 7
1716necon3ai 2638 . . . . . 6
18173ad2ant3 980 . . . . 5
1918intnand 883 . . . 4
20 df-nel 2601 . . . . 5
21 sseq2 3362 . . . . . . 7
2221elrab 3084 . . . . . 6
2322notbii 288 . . . . 5
2420, 23bitr2i 242 . . . 4
2519, 24sylib 189 . . 3
26 sseq2 3362 . . . . . . 7
2726elrab 3084 . . . . . 6
28 sseq2 3362 . . . . . . 7
2928elrab 3084 . . . . . 6
3027, 29anbi12i 679 . . . . 5
31 simpl 444 . . . . . . . . . . 11
32 simprll 739 . . . . . . . . . . 11
33 simprrl 741 . . . . . . . . . . 11
34 inopn 16964 . . . . . . . . . . 11
3531, 32, 33, 34syl3anc 1184 . . . . . . . . . 10
36 ssin 3555 . . . . . . . . . . . . 13
3736biimpi 187 . . . . . . . . . . . 12
3837ad2ant2l 727 . . . . . . . . . . 11
3938adantl 453 . . . . . . . . . 10
4035, 39jca 519 . . . . . . . . 9
41403ad2antl1 1119 . . . . . . . 8
42 sseq2 3362 . . . . . . . . 9
4342elrab 3084 . . . . . . . 8
4441, 43sylibr 204 . . . . . . 7
45 ssid 3359 . . . . . . 7
46 sseq1 3361 . . . . . . . 8
4746rspcev 3044 . . . . . . 7
4844, 45, 47sylancl 644 . . . . . 6
4948ex 424 . . . . 5
5030, 49syl5bi 209 . . . 4
5150ralrimivv 2789 . . 3
5215, 25, 513jca 1134 . 2
53 isfbas2 17859 . . . 4
548, 53syl 16 . . 3