Database
BASIC TOPOLOGY
Topology
Neighborhoods
opnneiid
Next ⟩
neissex
Metamath Proof Explorer
Ascii
Unicode
Theorem
opnneiid
Description:
Only an open set is a neighborhood of itself.
(Contributed by
FL
, 2-Oct-2006)
Ref
Expression
Assertion
opnneiid
⊢
J
∈
Top
→
N
∈
nei
⁡
J
⁡
N
↔
N
∈
J
Proof
Step
Hyp
Ref
Expression
1
neii2
⊢
J
∈
Top
∧
N
∈
nei
⁡
J
⁡
N
→
∃
x
∈
J
N
⊆
x
∧
x
⊆
N
2
eqss
⊢
N
=
x
↔
N
⊆
x
∧
x
⊆
N
3
eleq1a
⊢
x
∈
J
→
N
=
x
→
N
∈
J
4
2
3
syl5bir
⊢
x
∈
J
→
N
⊆
x
∧
x
⊆
N
→
N
∈
J
5
4
rexlimiv
⊢
∃
x
∈
J
N
⊆
x
∧
x
⊆
N
→
N
∈
J
6
1
5
syl
⊢
J
∈
Top
∧
N
∈
nei
⁡
J
⁡
N
→
N
∈
J
7
6
ex
⊢
J
∈
Top
→
N
∈
nei
⁡
J
⁡
N
→
N
∈
J
8
ssid
⊢
N
⊆
N
9
opnneiss
⊢
J
∈
Top
∧
N
∈
J
∧
N
⊆
N
→
N
∈
nei
⁡
J
⁡
N
10
9
3exp
⊢
J
∈
Top
→
N
∈
J
→
N
⊆
N
→
N
∈
nei
⁡
J
⁡
N
11
8
10
mpii
⊢
J
∈
Top
→
N
∈
J
→
N
∈
nei
⁡
J
⁡
N
12
7
11
impbid
⊢
J
∈
Top
→
N
∈
nei
⁡
J
⁡
N
↔
N
∈
J