Theorem ntr0

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

	Ref	Expression
Assertion	ntr0	$$⊢J\in \mathrm{Top}\to \mathrm{int}\left(J\right)\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0opn	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$
2		0ss	$$⊢\varnothing \subseteq \bigcup J$$
3		eqid	$$⊢\bigcup J=\bigcup J$$
4	3	isopn3	$$⊢\left(J\in \mathrm{Top}\wedge \varnothing \subseteq \bigcup J\right)\to \left(\varnothing \in J\leftrightarrow \mathrm{int}\left(J\right)\left(\varnothing \right)=\varnothing \right)$$
5	2 4	mpan2	$$⊢J\in \mathrm{Top}\to \left(\varnothing \in J\leftrightarrow \mathrm{int}\left(J\right)\left(\varnothing \right)=\varnothing \right)$$
6	1 5	mpbid	$$⊢J\in \mathrm{Top}\to \mathrm{int}\left(J\right)\left(\varnothing \right)=\varnothing$$