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 = ⋃ J$
	Assertion	isopn3	$⊢ (J \in Top \land S \subseteq X) \to (S \in J \leftrightarrow int (J) (S) = S)$

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2	1	ntrval	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) = ⋃ (J \cap 𝒫 S)$
3		inss2	$⊢ J \cap 𝒫 S \subseteq 𝒫 S$
4	3	unissi	$⊢ ⋃ (J \cap 𝒫 S) \subseteq ⋃ 𝒫 S$
5		unipw	$⊢ ⋃ 𝒫 S = S$
6	4 5	sseqtri	$⊢ ⋃ (J \cap 𝒫 S) \subseteq S$
7	6	a1i	$⊢ S \in J \to ⋃ (J \cap 𝒫 S) \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 (J \cap 𝒫 S)$
11		elssuni	$⊢ S \in (J \cap 𝒫 S) \to S \subseteq ⋃ (J \cap 𝒫 S)$
12	10 11	syl	$⊢ S \in J \to S \subseteq ⋃ (J \cap 𝒫 S)$
13	7 12	eqssd	$⊢ S \in J \to ⋃ (J \cap 𝒫 S) = S$
14	2 13	sylan9eq	$⊢ ((J \in Top \land S \subseteq X) \land S \in J) \to int (J) (S) = S$
15	14	ex	$⊢ (J \in Top \land S \subseteq X) \to (S \in J \to int (J) (S) = S)$
16	1	ntropn	$⊢ (J \in Top \land S \subseteq X) \to int (J) (S) \in J$
17		eleq1	$⊢ int (J) (S) = S \to (int (J) (S) \in J \leftrightarrow S \in J)$
18	16 17	syl5ibcom	$⊢ (J \in Top \land S \subseteq X) \to (int (J) (S) = S \to S \in J)$
19	15 18	impbid	$⊢ (J \in Top \land S \subseteq X) \to (S \in J \leftrightarrow int (J) (S) = S)$

Metamath Proof Explorer