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 ) ` (/) ) = (/) )