![]() |
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 20921 | . 2 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | |
2 | iscld.1 | . . . 4 ⊢ 𝑋 = ∪ 𝐽 | |
3 | 2 | iscld 20922 | . . 3 ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) |
4 | 3 | simprbda 654 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ 𝑋) |
5 | 1, 4 | mpancom 706 | 1 ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1564 ∈ wcel 2071 ∖ cdif 3645 ⊆ wss 3648 ∪ cuni 4512 ‘cfv 5969 Topctop 20789 Clsdccld 20911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-8 2073 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-sep 4857 ax-nul 4865 ax-pow 4916 ax-pr 4979 ax-un 7034 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-eu 2543 df-mo 2544 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ne 2865 df-ral 2987 df-rex 2988 df-rab 2991 df-v 3274 df-sbc 3510 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-nul 3992 df-if 4163 df-pw 4236 df-sn 4254 df-pr 4256 df-op 4260 df-uni 4513 df-br 4729 df-opab 4789 df-mpt 4806 df-id 5096 df-xp 5192 df-rel 5193 df-cnv 5194 df-co 5195 df-dm 5196 df-iota 5932 df-fun 5971 df-fn 5972 df-fv 5977 df-top 20790 df-cld 20914 |
This theorem is referenced by: cldss2 20925 iincld 20934 uncld 20936 cldcls 20937 iuncld 20940 clsval2 20945 clsss3 20954 clsss2 20967 opncldf1 20979 restcldr 21069 lmcld 21198 nrmsep2 21251 nrmsep 21252 isnrm2 21253 regsep2 21271 cmpcld 21296 dfconn2 21313 conncompclo 21329 cldllycmp 21389 txcld 21497 ptcld 21507 imasncld 21585 kqcldsat 21627 kqnrmlem1 21637 kqnrmlem2 21638 nrmhmph 21688 ufildr 21825 metnrmlem1a 22751 metnrmlem1 22752 metnrmlem2 22753 metnrmlem3 22754 cnheiborlem 22843 cmetss 23202 bcthlem5 23214 cldssbrsiga 30448 clsun 32518 cldregopn 32521 mblfinlem3 33648 mblfinlem4 33649 ismblfin 33650 cmpfiiin 37647 kelac1 38020 stoweidlem18 40623 stoweidlem57 40662 |
Copyright terms: Public domain | W3C validator |