Definition df-cmp 22547

Description: Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite subcovering (Heine-Borel property). Definition C''' of [BourbakiTop1] p. I.59. Note: Bourbaki uses the term "quasi-compact" (saving "compact" for "compact Hausdorff"), but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.)

Assertion

Ref	Expression
df-cmp	⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cmp

Step	Hyp	Ref	Expression
1		ccmp 22546	. 2 class Comp
2		vx	. . . . . . . 8 setvar 𝑥
3	2	cv 1538	. . . . . . 7 class 𝑥
4	3	cuni 4840	. . . . . 6 class ∪ 𝑥
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1538	. . . . . . 7 class 𝑦
7	6	cuni 4840	. . . . . 6 class ∪ 𝑦
8	4, 7	wceq 1539	. . . . 5 wff ∪ 𝑥 = ∪ 𝑦
9		vz	. . . . . . . . 9 setvar 𝑧
10	9	cv 1538	. . . . . . . 8 class 𝑧
11	10	cuni 4840	. . . . . . 7 class ∪ 𝑧
12	4, 11	wceq 1539	. . . . . 6 wff ∪ 𝑥 = ∪ 𝑧
13	6	cpw 4534	. . . . . . 7 class 𝒫 𝑦
14		cfn 8742	. . . . . . 7 class Fin
15	13, 14	cin 3887	. . . . . 6 class (𝒫 𝑦 ∩ Fin)
16	12, 9, 15	wrex 3066	. . . . 5 wff ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧
17	8, 16	wi 4	. . . 4 wff (∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)
18	3	cpw 4534	. . . 4 class 𝒫 𝑥
19	17, 5, 18	wral 3065	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)
20		ctop 22051	. . 3 class Top
21	19, 2, 20	crab 3069	. 2 class {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
22	1, 21	wceq 1539	1 wff Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}

This definition is referenced by:  iscmp  22548