![]() |
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 23058 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) |
3 | inss2 4253 | . . . 4 ⊢ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝒫 𝑆 | |
4 | 3 | unissi 4940 | . . 3 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ ∪ 𝒫 𝑆 |
5 | unipw 5473 | . . 3 ⊢ ∪ 𝒫 𝑆 = 𝑆 | |
6 | 4, 5 | sseqtri 4039 | . 2 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝑆 |
7 | 2, 6 | eqsstrdi 4057 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2103 ∩ cin 3969 ⊆ wss 3970 𝒫 cpw 4622 ∪ cuni 4931 ‘cfv 6572 Topctop 22913 intcnt 23039 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-rep 5306 ax-sep 5320 ax-nul 5327 ax-pow 5386 ax-pr 5450 ax-un 7766 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3384 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5021 df-br 5170 df-opab 5232 df-mpt 5253 df-id 5597 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-rn 5710 df-res 5711 df-ima 5712 df-iota 6524 df-fun 6574 df-fn 6575 df-f 6576 df-f1 6577 df-fo 6578 df-f1o 6579 df-fv 6580 df-top 22914 df-ntr 23042 |
This theorem is referenced by: ntrin 23083 neiint 23126 opnnei 23142 topssnei 23146 maxlp 23169 restntr 23204 iscnp4 23285 cnntri 23293 cnntr 23297 cnprest 23311 llycmpkgen2 23572 xkococnlem 23681 flimopn 23997 fclsneii 24039 fcfnei 24057 subgntr 24129 iccntr 24855 rectbntr0 24866 bcthlem5 25374 limcflf 25928 dvbss 25948 perfdvf 25950 dvreslem 25956 dvcnp2 25967 dvcnp2OLD 25968 dvnres 25979 dvaddbr 25986 dvcmulf 25994 dvmptres2 26012 dvmptcmul 26014 dvmptntr 26021 dvcnvre 26070 taylthlem1 26425 taylthlem2 26426 taylthlem2OLD 26427 ulmdvlem3 26455 lgamucov2 27091 ubthlem1 30893 kur14lem6 35171 cvmlift2lem12 35274 opnbnd 36238 opnregcld 36243 cldregopn 36244 dvresntr 45773 |
Copyright terms: Public domain | W3C validator |