Theorem ntropn

Description: The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$$⊢X=\bigcup J$$
2	1	ntrval	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \mathrm{int}\left(J\right)\left(S\right)=\bigcup \left(J\cap 𝒫S\right)$$
3		inss1	$$⊢J\cap 𝒫S\subseteq J$$
4		uniopn	$$⊢\left(J\in \mathrm{Top}\wedge J\cap 𝒫S\subseteq J\right)\to \bigcup \left(J\cap 𝒫S\right)\in J$$
5	3 4	mpan2	$$⊢J\in \mathrm{Top}\to \bigcup \left(J\cap 𝒫S\right)\in J$$
6	5	adantr	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \bigcup \left(J\cap 𝒫S\right)\in J$$
7	2 6	eqeltrd	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \mathrm{int}\left(J\right)\left(S\right)\in J$$