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

Definition df-cmp 21996
 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.)
Assertion
Ref Expression
df-cmp Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cmp
StepHypRef Expression
1 ccmp 21995 . 2 class Comp
2 vx . . . . . . . 8 setvar 𝑥
32cv 1537 . . . . . . 7 class 𝑥
43cuni 4803 . . . . . 6 class 𝑥
5 vy . . . . . . . 8 setvar 𝑦
65cv 1537 . . . . . . 7 class 𝑦
76cuni 4803 . . . . . 6 class 𝑦
84, 7wceq 1538 . . . . 5 wff 𝑥 = 𝑦
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1537 . . . . . . . 8 class 𝑧
1110cuni 4803 . . . . . . 7 class 𝑧
124, 11wceq 1538 . . . . . 6 wff 𝑥 = 𝑧
136cpw 4500 . . . . . . 7 class 𝒫 𝑦
14 cfn 8496 . . . . . . 7 class Fin
1513, 14cin 3883 . . . . . 6 class (𝒫 𝑦 ∩ Fin)
1612, 9, 15wrex 3110 . . . . 5 wff 𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧
178, 16wi 4 . . . 4 wff ( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)
183cpw 4500 . . . 4 class 𝒫 𝑥
1917, 5, 18wral 3109 . . 3 wff 𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)
20 ctop 21502 . . 3 class Top
2119, 2, 20crab 3113 . 2 class {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
221, 21wceq 1538 1 wff Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
 Colors of variables: wff setvar class This definition is referenced by:  iscmp  21997
 Copyright terms: Public domain W3C validator