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

Definition df-cmp 21398
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" 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 21397 . 2 class Comp
2 vx . . . . . . . 8 setvar 𝑥
32cv 1636 . . . . . . 7 class 𝑥
43cuni 4623 . . . . . 6 class 𝑥
5 vy . . . . . . . 8 setvar 𝑦
65cv 1636 . . . . . . 7 class 𝑦
76cuni 4623 . . . . . 6 class 𝑦
84, 7wceq 1637 . . . . 5 wff 𝑥 = 𝑦
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1636 . . . . . . . 8 class 𝑧
1110cuni 4623 . . . . . . 7 class 𝑧
124, 11wceq 1637 . . . . . 6 wff 𝑥 = 𝑧
136cpw 4345 . . . . . . 7 class 𝒫 𝑦
14 cfn 8186 . . . . . . 7 class Fin
1513, 14cin 3762 . . . . . 6 class (𝒫 𝑦 ∩ Fin)
1612, 9, 15wrex 3093 . . . . 5 wff 𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧
178, 16wi 4 . . . 4 wff ( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)
183cpw 4345 . . . 4 class 𝒫 𝑥
1917, 5, 18wral 3092 . . 3 wff 𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)
20 ctop 20905 . . 3 class Top
2119, 2, 20crab 3096 . 2 class {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
221, 21wceq 1637 1 wff Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin) 𝑥 = 𝑧)}
Colors of variables: wff setvar class
This definition is referenced by:  iscmp  21399
  Copyright terms: Public domain W3C validator