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

Definition df-cmp 16946
 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-cmp
StepHypRef Expression
1 ccmp 16945 . 2
2 vx . . . . . . . 8
32cv 1618 . . . . . . 7
43cuni 3727 . . . . . 6
5 vy . . . . . . . 8
65cv 1618 . . . . . . 7
76cuni 3727 . . . . . 6
84, 7wceq 1619 . . . . 5
9 vz . . . . . . . . 9
109cv 1618 . . . . . . . 8
1110cuni 3727 . . . . . . 7
124, 11wceq 1619 . . . . . 6
136cpw 3530 . . . . . . 7
14 cfn 6749 . . . . . . 7
1513, 14cin 3077 . . . . . 6
1612, 9, 15wrex 2510 . . . . 5
178, 16wi 6 . . . 4
183cpw 3530 . . . 4
1917, 5, 18wral 2509 . . 3
20 ctop 16463 . . 3
2119, 2, 20crab 2512 . 2
221, 21wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  iscmp  16947
 Copyright terms: Public domain W3C validator