Definition df-cmp 17404

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). Definition C''' of [BourbakiTop1] p. I.59. Note: Bourbaki uses the term quasi-compact topology but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.)

Assertion

Ref	Expression
df-cmp	|- Comp = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-cmp

Step	Hyp	Ref	Expression
1		ccmp 17403	. 2 class Comp
2		vx	. . . . . . . 8 set x
3	2	cv 1648	. . . . . . 7 class x
4	3	cuni 3975	. . . . . 6 class U. x
5		vy	. . . . . . . 8 set y
6	5	cv 1648	. . . . . . 7 class y
7	6	cuni 3975	. . . . . 6 class U. y
8	4, 7	wceq 1649	. . . . 5 wff U. x = U. y
9		vz	. . . . . . . . 9 set z
10	9	cv 1648	. . . . . . . 8 class z
11	10	cuni 3975	. . . . . . 7 class U. z
12	4, 11	wceq 1649	. . . . . 6 wff U. x = U. z
13	6	cpw 3759	. . . . . . 7 class ~P y
14		cfn 7068	. . . . . . 7 class Fin
15	13, 14	cin 3279	. . . . . 6 class ( ~P y i^i Fin )
16	12, 9, 15	wrex 2667	. . . . 5 wff E. z e. ( ~P y i^i Fin ) U. x = U. z
17	8, 16	wi 4	. . . 4 wff ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z )
18	3	cpw 3759	. . . 4 class ~P x
19	17, 5, 18	wral 2666	. . 3 wff A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z )
20		ctop 16913	. . 3 class Top
21	19, 2, 20	crab 2670	. 2 class { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
22	1, 21	wceq 1649	1 wff Comp = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }

This definition is referenced by:  iscmp  17405