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	⊢ 𝑋 = ∪ 𝐽
Assertion	isopn3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	ntrval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
3		inss2	⊢ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝒫 𝑆
4	3	unissi	⊢ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ ∪ 𝒫 𝑆
5		unipw	⊢ ∪ 𝒫 𝑆 = 𝑆
6	4 5	sseqtri	⊢ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆
7	6	a1i	⊢ ( 𝑆 ∈ 𝐽 → ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆 )
8		id	⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ∈ 𝐽 )
9		pwidg	⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ∈ 𝒫 𝑆 )
10	8 9	elind	⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) )
11		elssuni	⊢ ( 𝑆 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) → 𝑆 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
12	10 11	syl	⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
13	7 12	eqssd	⊢ ( 𝑆 ∈ 𝐽 → ∪ ( 𝐽 ∩ 𝒫 𝑆 ) = 𝑆 )
14	2 13	sylan9eq	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )
15	14	ex	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐽 → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
16	1	ntropn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )
17		eleq1	⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ↔ 𝑆 ∈ 𝐽 ) )
18	16 17	syl5ibcom	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 → 𝑆 ∈ 𝐽 ) )
19	15 18	impbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )