This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) }