Definition df-cmp

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)

	Ref	Expression
Assertion	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 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccmp	|- Comp
1		vx	|- x
2		ctop	|- Top
3		vy	|- y
4	1	cv	|- x
5	4	cpw	|- ~P x
6	4	cuni	|- U. x
7	3	cv	|- y
8	7	cuni	|- U. y
9	6 8	wceq	|- U. x = U. y
10		vz	|- z
11	7	cpw	|- ~P y
12		cfn	|- Fin
13	11 12	cin	|- ( ~P y i^i Fin )
14	10	cv	|- z
15	14	cuni	|- U. z
16	6 15	wceq	|- U. x = U. z
17	16 10 13	wrex	|- E. z e. ( ~P y i^i Fin ) U. x = U. z
18	9 17	wi	|- ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z )
19	18 3 5	wral	|- A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z )
20	19 1 2	crab	|- { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
21	0 20	wceq	|- 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 ) }