![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iscmp | Structured version Visualization version GIF version |
Description: The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
Ref | Expression |
---|---|
iscmp.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
iscmp | ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 4579 | . . 3 ⊢ (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽) | |
2 | unieq 4881 | . . . . . 6 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽) | |
3 | iscmp.1 | . . . . . 6 ⊢ 𝑋 = ∪ 𝐽 | |
4 | 2, 3 | eqtr4di 2789 | . . . . 5 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = 𝑋) |
5 | 4 | eqeq1d 2733 | . . . 4 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦)) |
6 | 4 | eqeq1d 2733 | . . . . 5 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧)) |
7 | 6 | rexbidv 3171 | . . . 4 ⊢ (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
8 | 5, 7 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝐽 → ((∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
9 | 1, 8 | raleqbidv 3317 | . 2 ⊢ (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
10 | df-cmp 22775 | . 2 ⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)} | |
11 | 9, 10 | elrab2 3651 | 1 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 ∩ cin 3912 𝒫 cpw 4565 ∪ cuni 4870 Fincfn 8890 Topctop 22279 Compccmp 22774 |
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-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3406 df-v 3448 df-in 3920 df-ss 3930 df-pw 4567 df-uni 4871 df-cmp 22775 |
This theorem is referenced by: cmpcov 22777 cncmp 22780 fincmp 22781 cmptop 22783 cmpsub 22788 tgcmp 22789 uncmp 22791 sscmp 22793 cmpfi 22796 comppfsc 22920 txcmp 23031 alexsubb 23434 alexsubALT 23439 cmpcref 32520 onsucsuccmpi 34991 limsucncmpi 34993 pibp16 35957 heibor 36353 |
Copyright terms: Public domain | W3C validator |