![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isopn3 | Structured version Visualization version GIF version |
Description: A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
Ref | Expression |
---|---|
clscld.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
isopn3 | ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clscld.1 | . . . . 5 ⊢ 𝑋 = ∪ 𝐽 | |
2 | 1 | ntrval 21316 | . . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) |
3 | inss2 4121 | . . . . . . . 8 ⊢ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝒫 𝑆 | |
4 | 3 | unissi 4762 | . . . . . . 7 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ ∪ 𝒫 𝑆 |
5 | unipw 5227 | . . . . . . 7 ⊢ ∪ 𝒫 𝑆 = 𝑆 | |
6 | 4, 5 | sseqtri 3919 | . . . . . 6 ⊢ ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝑆 |
7 | 6 | a1i 11 | . . . . 5 ⊢ (𝑆 ∈ 𝐽 → ∪ (𝐽 ∩ 𝒫 𝑆) ⊆ 𝑆) |
8 | id 22 | . . . . . . 7 ⊢ (𝑆 ∈ 𝐽 → 𝑆 ∈ 𝐽) | |
9 | pwidg 4462 | . . . . . . 7 ⊢ (𝑆 ∈ 𝐽 → 𝑆 ∈ 𝒫 𝑆) | |
10 | 8, 9 | elind 4087 | . . . . . 6 ⊢ (𝑆 ∈ 𝐽 → 𝑆 ∈ (𝐽 ∩ 𝒫 𝑆)) |
11 | elssuni 4768 | . . . . . 6 ⊢ (𝑆 ∈ (𝐽 ∩ 𝒫 𝑆) → 𝑆 ⊆ ∪ (𝐽 ∩ 𝒫 𝑆)) | |
12 | 10, 11 | syl 17 | . . . . 5 ⊢ (𝑆 ∈ 𝐽 → 𝑆 ⊆ ∪ (𝐽 ∩ 𝒫 𝑆)) |
13 | 7, 12 | eqssd 3901 | . . . 4 ⊢ (𝑆 ∈ 𝐽 → ∪ (𝐽 ∩ 𝒫 𝑆) = 𝑆) |
14 | 2, 13 | sylan9eq 2849 | . . 3 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) |
15 | 14 | ex 413 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 → ((int‘𝐽)‘𝑆) = 𝑆)) |
16 | 1 | ntropn 21329 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ∈ 𝐽) |
17 | eleq1 2868 | . . 3 ⊢ (((int‘𝐽)‘𝑆) = 𝑆 → (((int‘𝐽)‘𝑆) ∈ 𝐽 ↔ 𝑆 ∈ 𝐽)) | |
18 | 16, 17 | syl5ibcom 246 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = 𝑆 → 𝑆 ∈ 𝐽)) |
19 | 15, 18 | impbid 213 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1520 ∈ wcel 2079 ∩ cin 3853 ⊆ wss 3854 𝒫 cpw 4447 ∪ cuni 4739 ‘cfv 6217 Topctop 21173 intcnt 21297 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-ral 3108 df-rex 3109 df-reu 3110 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-top 21174 df-ntr 21300 |
This theorem is referenced by: ntridm 21348 ntrtop 21350 ntr0 21361 isopn3i 21362 opnnei 21400 cnntr 21555 llycmpkgen2 21830 dvnres 24199 dvcnvre 24287 taylthlem2 24633 ulmdvlem3 24661 abelth 24700 opnbnd 33227 ioontr 41283 cncfuni 41664 fperdvper 41698 dirkercncflem3 41886 dirkercncflem4 41887 fourierdlem58 41945 fourierdlem73 41960 |
Copyright terms: Public domain | W3C validator |