Metamath Proof Explorer


Theorem ntr0

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

Ref Expression
Assertion ntr0 JTopintJ=

Proof

Step Hyp Ref Expression
1 0opn JTopJ
2 0ss J
3 eqid J=J
4 3 isopn3 JTopJJintJ=
5 2 4 mpan2 JTopJintJ=
6 1 5 mpbid JTopintJ=