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 =