MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cmp Unicode version

Definition df-cmp 17077
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
StepHypRef Expression
1 ccmp 17076 . 2  class  Comp
2 vx . . . . . . . 8  set  x
32cv 1618 . . . . . . 7  class  x
43cuni 3801 . . . . . 6  class  U. x
5 vy . . . . . . . 8  set  y
65cv 1618 . . . . . . 7  class  y
76cuni 3801 . . . . . 6  class  U. y
84, 7wceq 1619 . . . . 5  wff  U. x  =  U. y
9 vz . . . . . . . . 9  set  z
109cv 1618 . . . . . . . 8  class  z
1110cuni 3801 . . . . . . 7  class  U. z
124, 11wceq 1619 . . . . . 6  wff  U. x  =  U. z
136cpw 3599 . . . . . . 7  class  ~P y
14 cfn 6831 . . . . . . 7  class  Fin
1513, 14cin 3126 . . . . . 6  class  ( ~P y  i^i  Fin )
1612, 9, 15wrex 2519 . . . . 5  wff  E. z  e.  ( ~P y  i^i 
Fin ) U. x  =  U. z
178, 16wi 6 . . . 4  wff  ( U. x  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) U. x  =  U. z )
183cpw 3599 . . . 4  class  ~P x
1917, 5, 18wral 2518 . . 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 16594 . . 3  class  Top
2119, 2, 20crab 2522 . 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 ) }
221, 21wceq 1619 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 ) }
Colors of variables: wff set class
This definition is referenced by:  iscmp  17078
  Copyright terms: Public domain W3C validator