This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐽 ) ‘ 𝑆 ) )