Database
BASIC TOPOLOGY
Topology
Neighborhoods
neii2
Next ⟩
neiss
Metamath Proof Explorer
Ascii
Unicode
Theorem
neii2
Description:
Property of a neighborhood.
(Contributed by
NM
, 12-Feb-2007)
Ref
Expression
Assertion
neii2
⊢
J
∈
Top
∧
N
∈
nei
⁡
J
⁡
S
→
∃
g
∈
J
S
⊆
g
∧
g
⊆
N
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
⋃
J
=
⋃
J
2
1
neiss2
⊢
J
∈
Top
∧
N
∈
nei
⁡
J
⁡
S
→
S
⊆
⋃
J
3
1
isnei
⊢
J
∈
Top
∧
S
⊆
⋃
J
→
N
∈
nei
⁡
J
⁡
S
↔
N
⊆
⋃
J
∧
∃
g
∈
J
S
⊆
g
∧
g
⊆
N
4
simpr
⊢
N
⊆
⋃
J
∧
∃
g
∈
J
S
⊆
g
∧
g
⊆
N
→
∃
g
∈
J
S
⊆
g
∧
g
⊆
N
5
3
4
syl6bi
⊢
J
∈
Top
∧
S
⊆
⋃
J
→
N
∈
nei
⁡
J
⁡
S
→
∃
g
∈
J
S
⊆
g
∧
g
⊆
N
6
5
impancom
⊢
J
∈
Top
∧
N
∈
nei
⁡
J
⁡
S
→
S
⊆
⋃
J
→
∃
g
∈
J
S
⊆
g
∧
g
⊆
N
7
2
6
mpd
⊢
J
∈
Top
∧
N
∈
nei
⁡
J
⁡
S
→
∃
g
∈
J
S
⊆
g
∧
g
⊆
N