This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⁡ ∅ = ∅