Metamath Proof Explorer


Theorem ntr0

Description: The interior of the empty set. (Contributed by NM, 2-Oct-2007)

Ref Expression
Assertion ntr0 ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ )

Proof

Step Hyp Ref Expression
1 0opn ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
2 0ss ∅ ⊆ 𝐽
3 eqid 𝐽 = 𝐽
4 3 isopn3 ( ( 𝐽 ∈ Top ∧ ∅ ⊆ 𝐽 ) → ( ∅ ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ ) )
5 2 4 mpan2 ( 𝐽 ∈ Top → ( ∅ ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ ) )
6 1 5 mpbid ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ )