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 22139 | . 2 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑟 ∈ 𝒫 𝐽(∪ 𝐽 = ∪ 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)∪ 𝐽 = ∪ 𝑠))) |
3 | 2 | simplbi 501 | 1 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ∀wral 3053 ∃wrex 3054 ∩ cin 3842 𝒫 cpw 4488 ∪ cuni 4796 Fincfn 8555 Topctop 21644 Compccmp 22137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-in 3850 df-ss 3860 df-pw 4490 df-uni 4797 df-cmp 22138 |
This theorem is referenced by: imacmp 22148 cmpcld 22153 fiuncmp 22155 cmpfii 22160 bwth 22161 locfincmp 22277 kgeni 22288 kgentopon 22289 kgencmp 22296 kgencmp2 22297 cmpkgen 22302 txcmplem1 22392 txcmp 22394 qtopcmp 22459 cmphaushmeo 22551 ptcmpfi 22564 fclscmpi 22780 alexsubALTlem1 22798 ptcmplem1 22803 ptcmpg 22808 evth 23711 evth2 23712 cmppcmp 31380 ordcmp 34274 poimirlem30 35430 heibor1lem 35590 cmpfiiin 40091 kelac1 40460 kelac2 40462 stoweidlem28 43111 stoweidlem50 43133 stoweidlem53 43136 stoweidlem57 43140 stoweidlem62 43145 |
Copyright terms: Public domain | W3C validator |