| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ntrss2 | Structured version Visualization version GIF version | ||
| Description: A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
| Ref | Expression |
|---|---|
| clscld.1 | ⊢ 𝑋 = ∪ 𝐽 |
| Ref | Expression |
|---|---|
| ntrss2 | ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clscld.1 | . . 3 ⊢ 𝑋 = ∪ 𝐽 | |
| 2 | 1 | ntrval 22929 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) |
| 3 | inss2 4203 | . . . 4 ⊢ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝒫 𝑆 | |
| 4 | 3 | unissi 4882 | . . 3 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ ∪ 𝒫 𝑆 |
| 5 | unipw 5412 | . . 3 ⊢ ∪ 𝒫 𝑆 = 𝑆 | |
| 6 | 4, 5 | sseqtri 3997 | . 2 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝑆 |
| 7 | 2, 6 | eqsstrdi 3993 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∩ cin 3915 ⊆ wss 3916 𝒫 cpw 4565 ∪ cuni 4873 ‘cfv 6513 Topctop 22786 intcnt 22910 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5236 ax-sep 5253 ax-nul 5263 ax-pow 5322 ax-pr 5389 ax-un 7713 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3756 df-csb 3865 df-dif 3919 df-un 3921 df-in 3923 df-ss 3933 df-nul 4299 df-if 4491 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5110 df-opab 5172 df-mpt 5191 df-id 5535 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-iota 6466 df-fun 6515 df-fn 6516 df-f 6517 df-f1 6518 df-fo 6519 df-f1o 6520 df-fv 6521 df-top 22787 df-ntr 22913 |
| This theorem is referenced by: ntrin 22954 neiint 22997 opnnei 23013 topssnei 23017 maxlp 23040 restntr 23075 iscnp4 23156 cnntri 23164 cnntr 23168 cnprest 23182 llycmpkgen2 23443 xkococnlem 23552 flimopn 23868 fclsneii 23910 fcfnei 23928 subgntr 24000 iccntr 24716 rectbntr0 24727 bcthlem5 25234 limcflf 25788 dvbss 25808 perfdvf 25810 dvreslem 25816 dvcnp2 25827 dvcnp2OLD 25828 dvnres 25839 dvaddbr 25846 dvcmulf 25854 dvmptres2 25872 dvmptcmul 25874 dvmptntr 25881 dvcnvre 25930 taylthlem1 26287 taylthlem2 26288 taylthlem2OLD 26289 ulmdvlem3 26317 lgamucov2 26955 ubthlem1 30805 kur14lem6 35198 cvmlift2lem12 35301 opnbnd 36308 opnregcld 36313 cldregopn 36314 dvresntr 45909 |
| Copyright terms: Public domain | W3C validator |