Database
BASIC TOPOLOGY
Topology
Neighborhoods
opnneiss
Next ⟩
opnneip
Metamath Proof Explorer
Ascii
Unicode
Theorem
opnneiss
Description:
An open set is a neighborhood of any of its subsets.
(Contributed by
NM
, 13-Feb-2007)
Ref
Expression
Assertion
opnneiss
⊢
J
∈
Top
∧
N
∈
J
∧
S
⊆
N
→
N
∈
nei
⁡
J
⁡
S
Proof
Step
Hyp
Ref
Expression
1
simp3
⊢
J
∈
Top
∧
N
∈
J
∧
S
⊆
N
→
S
⊆
N
2
eqid
⊢
⋃
J
=
⋃
J
3
2
eltopss
⊢
J
∈
Top
∧
N
∈
J
→
N
⊆
⋃
J
4
sstr
⊢
S
⊆
N
∧
N
⊆
⋃
J
→
S
⊆
⋃
J
5
4
ancoms
⊢
N
⊆
⋃
J
∧
S
⊆
N
→
S
⊆
⋃
J
6
3
5
stoic3
⊢
J
∈
Top
∧
N
∈
J
∧
S
⊆
N
→
S
⊆
⋃
J
7
2
opnneissb
⊢
J
∈
Top
∧
N
∈
J
∧
S
⊆
⋃
J
→
S
⊆
N
↔
N
∈
nei
⁡
J
⁡
S
8
6
7
syld3an3
⊢
J
∈
Top
∧
N
∈
J
∧
S
⊆
N
→
S
⊆
N
↔
N
∈
nei
⁡
J
⁡
S
9
1
8
mpbid
⊢
J
∈
Top
∧
N
∈
J
∧
S
⊆
N
→
N
∈
nei
⁡
J
⁡
S