This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007)
(Revised by Mario Carneiro, 11-Nov-2013)
|
|
Ref |
Expression |
|
Hypothesis |
clscld.1 |
⊢ 𝑋 = ∪ 𝐽 |
|
Assertion |
ntrss2 |
⊢ ( ( 𝐽 ∈ 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 |
2 6
|
eqsstrdi |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) |