Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cmptop | Structured version Visualization version GIF version |
Description: A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
Ref | Expression |
---|---|
cmptop | ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . 3 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | iscmp 22539 | . 2 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 = ∪ 𝑠))) |
3 | 2 | simplbi 498 | 1 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 ∩ cin 3886 𝒫 cpw 4533 ∪ cuni 4839 Fincfn 8733 Topctop 22042 Compccmp 22537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-in 3894 df-ss 3904 df-pw 4535 df-uni 4840 df-cmp 22538 |
This theorem is referenced by: imacmp 22548 cmpcld 22553 fiuncmp 22555 cmpfii 22560 bwth 22561 locfincmp 22677 kgeni 22688 kgentopon 22689 kgencmp 22696 kgencmp2 22697 cmpkgen 22702 txcmplem1 22792 txcmp 22794 qtopcmp 22859 cmphaushmeo 22951 ptcmpfi 22964 fclscmpi 23180 alexsubALTlem1 23198 ptcmplem1 23203 ptcmpg 23208 evth 24122 evth2 24123 cmppcmp 31808 ordcmp 34636 poimirlem30 35807 heibor1lem 35967 cmpfiiin 40519 kelac1 40888 kelac2 40890 stoweidlem28 43569 stoweidlem50 43591 stoweidlem53 43594 stoweidlem57 43598 stoweidlem62 43603 |
Copyright terms: Public domain | W3C validator |