![]() |
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 4574 | . . 3 ⊢ (𝑥 = 𝐽 → 𝒫 𝑥 = 𝒫 𝐽) | |
2 | unieq 4876 | . . . . . 6 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = ∪ 𝐽) | |
3 | iscmp.1 | . . . . . 6 ⊢ 𝑋 = ∪ 𝐽 | |
4 | 2, 3 | eqtr4di 2794 | . . . . 5 ⊢ (𝑥 = 𝐽 → ∪ 𝑥 = 𝑋) |
5 | 4 | eqeq1d 2738 | . . . 4 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝑦)) |
6 | 4 | eqeq1d 2738 | . . . . 5 ⊢ (𝑥 = 𝐽 → (∪ 𝑥 = ∪ 𝑧 ↔ 𝑋 = ∪ 𝑧)) |
7 | 6 | rexbidv 3175 | . . . 4 ⊢ (𝑥 = 𝐽 → (∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
8 | 5, 7 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝐽 → ((∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
9 | 1, 8 | raleqbidv 3319 | . 2 ⊢ (𝑥 = 𝐽 → (∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧) ↔ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
10 | df-cmp 22736 | . 2 ⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)} | |
11 | 9, 10 | elrab2 3648 | 1 ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 ∩ cin 3909 𝒫 cpw 4560 ∪ cuni 4865 Fincfn 8882 Topctop 22240 Compccmp 22735 |
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 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-in 3917 df-ss 3927 df-pw 4562 df-uni 4866 df-cmp 22736 |
This theorem is referenced by: cmpcov 22738 cncmp 22741 fincmp 22742 cmptop 22744 cmpsub 22749 tgcmp 22750 uncmp 22752 sscmp 22754 cmpfi 22757 comppfsc 22881 txcmp 22992 alexsubb 23395 alexsubALT 23400 cmpcref 32371 onsucsuccmpi 34905 limsucncmpi 34907 pibp16 35874 heibor 36270 |
Copyright terms: Public domain | W3C validator |