Theorem ntrtop

Description: The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006)

	Ref	Expression
Hypothesis	clscld.1	$$⊢X=\bigcup J$$
Assertion	ntrtop	$$⊢J\in \mathrm{Top}\to \mathrm{int}\left(J\right)\left(X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$$⊢X=\bigcup J$$
2	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
3		ssid	$$⊢X\subseteq X$$
4	1	isopn3	$$⊢\left(J\in \mathrm{Top}\wedge X\subseteq X\right)\to \left(X\in J\leftrightarrow \mathrm{int}\left(J\right)\left(X\right)=X\right)$$
5	3 4	mpan2	$$⊢J\in \mathrm{Top}\to \left(X\in J\leftrightarrow \mathrm{int}\left(J\right)\left(X\right)=X\right)$$
6	2 5	mpbid	$$⊢J\in \mathrm{Top}\to \mathrm{int}\left(J\right)\left(X\right)=X$$