Metamath Proof Explorer


Theorem ntr0

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

Ref Expression
Assertion ntr0
|- ( J e. Top -> ( ( int ` J ) ` (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 0opn
 |-  ( J e. Top -> (/) e. J )
2 0ss
 |-  (/) C_ U. J
3 eqid
 |-  U. J = U. J
4 3 isopn3
 |-  ( ( J e. Top /\ (/) C_ U. J ) -> ( (/) e. J <-> ( ( int ` J ) ` (/) ) = (/) ) )
5 2 4 mpan2
 |-  ( J e. Top -> ( (/) e. J <-> ( ( int ` J ) ` (/) ) = (/) ) )
6 1 5 mpbid
 |-  ( J e. Top -> ( ( int ` J ) ` (/) ) = (/) )