Theorem ssntr

Description: An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	ssntr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) ) → 𝑂 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2		elin	⊢ ( 𝑂 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) ↔ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ∈ 𝒫 𝑆 ) )
3		elpwg	⊢ ( 𝑂 ∈ 𝐽 → ( 𝑂 ∈ 𝒫 𝑆 ↔ 𝑂 ⊆ 𝑆 ) )
4	3	pm5.32i	⊢ ( ( 𝑂 ∈ 𝐽 ∧ 𝑂 ∈ 𝒫 𝑆 ) ↔ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) )
5	2 4	bitr2i	⊢ ( ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) ↔ 𝑂 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) )
6		elssuni	⊢ ( 𝑂 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) → 𝑂 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
7	5 6	sylbi	⊢ ( ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) → 𝑂 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
8	7	adantl	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) ) → 𝑂 ⊆ ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
9	1	ntrval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
10	9	adantr	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
11	8 10	sseqtrrd	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆 ) ) → 𝑂 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )