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

Definition df-cmp 17130
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 17129 . 2  class  Comp
2 vx . . . . . . . 8  set  x
32cv 1631 . . . . . . 7  class  x
43cuni 3843 . . . . . 6  class  U. x
5 vy . . . . . . . 8  set  y
65cv 1631 . . . . . . 7  class  y
76cuni 3843 . . . . . 6  class  U. y
84, 7wceq 1632 . . . . 5  wff  U. x  =  U. y
9 vz . . . . . . . . 9  set  z
109cv 1631 . . . . . . . 8  class  z
1110cuni 3843 . . . . . . 7  class  U. z
124, 11wceq 1632 . . . . . 6  wff  U. x  =  U. z
136cpw 3638 . . . . . . 7  class  ~P y
14 cfn 6879 . . . . . . 7  class  Fin
1513, 14cin 3164 . . . . . 6  class  ( ~P y  i^i  Fin )
1612, 9, 15wrex 2557 . . . . 5  wff  E. z  e.  ( ~P y  i^i 
Fin ) U. x  =  U. z
178, 16wi 4 . . . 4  wff  ( U. x  =  U. y  ->  E. z  e.  ( ~P y  i^i  Fin ) U. x  =  U. z )
183cpw 3638 . . . 4  class  ~P x
1917, 5, 18wral 2556 . . 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 16647 . . 3  class  Top
2119, 2, 20crab 2560 . 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 1632 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  17131
  Copyright terms: Public domain W3C validator