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

Definition df-cmp 17442
 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 17441 . 2
2 vx . . . . . . . 8
32cv 1651 . . . . . . 7
43cuni 4007 . . . . . 6
5 vy . . . . . . . 8
65cv 1651 . . . . . . 7
76cuni 4007 . . . . . 6
84, 7wceq 1652 . . . . 5
9 vz . . . . . . . . 9
109cv 1651 . . . . . . . 8
1110cuni 4007 . . . . . . 7
124, 11wceq 1652 . . . . . 6
136cpw 3791 . . . . . . 7
14 cfn 7101 . . . . . . 7
1513, 14cin 3311 . . . . . 6
1612, 9, 15wrex 2698 . . . . 5
178, 16wi 4 . . . 4
183cpw 3791 . . . 4
1917, 5, 18wral 2697 . . 3
20 ctop 16950 . . 3
2119, 2, 20crab 2701 . 2
221, 21wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  iscmp  17443
 Copyright terms: Public domain W3C validator