![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cldss | Structured version Visualization version GIF version |
Description: A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
Ref | Expression |
---|---|
iscld.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
cldss | ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cldrcl 22375 | . 2 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | |
2 | iscld.1 | . . . 4 ⊢ 𝑋 = ∪ 𝐽 | |
3 | 2 | iscld 22376 | . . 3 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) |
4 | 3 | simprbda 499 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ 𝑋) |
5 | 1, 4 | mpancom 686 | 1 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2106 ∖ cdif 3907 ⊆ wss 3910 ∪ cuni 4865 ‘cfv 6496 Topctop 22240 Clsdccld 22365 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7671 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fn 6499 df-fv 6504 df-top 22241 df-cld 22368 |
This theorem is referenced by: cldss2 22379 iincld 22388 uncld 22390 cldcls 22391 iuncld 22394 clsval2 22399 clsss3 22408 clsss2 22421 opncldf1 22433 restcldr 22523 lmcld 22652 nrmsep2 22705 nrmsep 22706 isnrm2 22707 regsep2 22725 cmpcld 22751 dfconn2 22768 conncompclo 22784 cldllycmp 22844 txcld 22952 ptcld 22962 imasncld 23040 kqcldsat 23082 kqnrmlem1 23092 kqnrmlem2 23093 nrmhmph 23143 ufildr 23280 metnrmlem1a 24219 metnrmlem1 24220 metnrmlem2 24221 metnrmlem3 24222 cnheiborlem 24315 cmetss 24678 bcthlem5 24690 cldssbrsiga 32777 clsun 34791 cldregopn 34794 pibt2 35879 mblfinlem3 36108 mblfinlem4 36109 ismblfin 36110 cmpfiiin 40998 kelac1 41368 stoweidlem18 44231 stoweidlem57 44270 restcls2lem 46917 |
Copyright terms: Public domain | W3C validator |