Database
BASIC TOPOLOGY
Topology
Closure and interior
ntr0
Next ⟩
isopn3i
Metamath Proof Explorer
Ascii
Unicode
Theorem
ntr0
Description:
The interior of the empty set.
(Contributed by
NM
, 2-Oct-2007)
Ref
Expression
Assertion
ntr0
⊢
J
∈
Top
→
int
⁡
J
⁡
∅
=
∅
Proof
Step
Hyp
Ref
Expression
1
0opn
⊢
J
∈
Top
→
∅
∈
J
2
0ss
⊢
∅
⊆
⋃
J
3
eqid
⊢
⋃
J
=
⋃
J
4
3
isopn3
⊢
J
∈
Top
∧
∅
⊆
⋃
J
→
∅
∈
J
↔
int
⁡
J
⁡
∅
=
∅
5
2
4
mpan2
⊢
J
∈
Top
→
∅
∈
J
↔
int
⁡
J
⁡
∅
=
∅
6
1
5
mpbid
⊢
J
∈
Top
→
int
⁡
J
⁡
∅
=
∅