Theorem ntrss2

Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007) (Revised by Mario Carneiro, 11-Nov-2013)

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

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		inss2	$$⊢J\cap 𝒫S\subseteq 𝒫S$$
4	3	unissi	$$⊢\bigcup \left(J\cap 𝒫S\right)\subseteq \bigcup 𝒫S$$
5		unipw	$$⊢\bigcup 𝒫S=S$$
6	4 5	sseqtri	$$⊢\bigcup \left(J\cap 𝒫S\right)\subseteq S$$
7	2 6	eqsstrdi	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \mathrm{int}\left(J\right)\left(S\right)\subseteq S$$