Definition df-comp 11113

Description: Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite sub-covering (Heine-Borel property). Bourbaki TG I.59 prop C''' . Note: Bourbaki uses the term quasi-compact topology but it is not the modern usage (which we follow).

Assertion

Ref	Expression
df-comp	⊢ Comp = {x ∈ Top∣∀y ∈ ℘ x(∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z)}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-comp

Step	Hyp	Ref	Expression
1		ccomp 11112	. 2 class Comp
2		vx	. . . . . . . 8 set x
3	2	cv 991	. . . . . . 7 class x
4	3	cuni 2569	. . . . . 6 class ∪x
5		vy	. . . . . . . 8 set y
6	5	cv 991	. . . . . . 7 class y
7	6	cuni 2569	. . . . . 6 class ∪y
8	4, 7	wceq 992	. . . . 5 wff ∪x = ∪y
9		vz	. . . . . . . . 9 set z
10	9	cv 991	. . . . . . . 8 class z
11	10	cuni 2569	. . . . . . 7 class ∪z
12	4, 11	wceq 992	. . . . . 6 wff ∪x = ∪z
13	6	cpw 2458	. . . . . . 7 class ℘y
14		cfn 4508	. . . . . . 7 class Fin
15	13, 14	cin 2098	. . . . . 6 class (℘y ∩ Fin)
16	12, 9, 15	wrex 1692	. . . . 5 wff ∃z ∈ (℘y ∩ Fin)∪x = ∪z
17	8, 16	wi 3	. . . 4 wff (∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z)
18	3	cpw 2458	. . . 4 class ℘x
19	17, 5, 18	wral 1691	. . 3 wff ∀y ∈ ℘ x(∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z)
20		ctop 7800	. . 3 class Top
21	19, 2, 20	crab 1694	. 2 class {x ∈ Top∣∀y ∈ ℘ x(∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z)}
22	1, 21	wceq 992	1 wff Comp = {x ∈ Top∣∀y ∈ ℘ x(∪x = ∪y → ∃z ∈ (℘y ∩ Fin)∪x = ∪z)}

This definition is referenced by:  iscomp 11114

Copyright terms: Public domain