Theorem isopn3

Description: A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

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	6	a1i	$$⊢S\in J\to \bigcup \left(J\cap 𝒫S\right)\subseteq S$$
8		id	$$⊢S\in J\to S\in J$$
9		pwidg	$$⊢S\in J\to S\in 𝒫S$$
10	8 9	elind	$$⊢S\in J\to S\in \left(J\cap 𝒫S\right)$$
11		elssuni	$$⊢S\in \left(J\cap 𝒫S\right)\to S\subseteq \bigcup \left(J\cap 𝒫S\right)$$
12	10 11	syl	$$⊢S\in J\to S\subseteq \bigcup \left(J\cap 𝒫S\right)$$
13	7 12	eqssd	$$⊢S\in J\to \bigcup \left(J\cap 𝒫S\right)=S$$
14	2 13	sylan9eq	$$⊢\left(\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\wedge S\in J\right)\to \mathrm{int}\left(J\right)\left(S\right)=S$$
15	14	ex	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \left(S\in J\to \mathrm{int}\left(J\right)\left(S\right)=S\right)$$
16	1	ntropn	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \mathrm{int}\left(J\right)\left(S\right)\in J$$
17		eleq1	$$⊢\mathrm{int}\left(J\right)\left(S\right)=S\to \left(\mathrm{int}\left(J\right)\left(S\right)\in J\leftrightarrow S\in J\right)$$
18	16 17	syl5ibcom	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \left(\mathrm{int}\left(J\right)\left(S\right)=S\to S\in J\right)$$
19	15 18	impbid	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq X\right)\to \left(S\in J\leftrightarrow \mathrm{int}\left(J\right)\left(S\right)=S\right)$$