This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cmp

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)

Ref Expression
Assertion df-cmp ⊢ Comp = x ∈ Top | ∀ y ∈ 𝒫 x ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmp class Comp
1 vx setvar x
2 ctop class Top
3 vy setvar y
4 1 cv setvar x
5 4 cpw class 𝒫 x
6 4 cuni class ⋃ x
7 3 cv setvar y
8 7 cuni class ⋃ y
9 6 8 wceq wff ⋃ x = ⋃ y
10 vz setvar z
11 7 cpw class 𝒫 y
12 cfn class Fin
13 11 12 cin class 𝒫 y ∩ Fin
14 10 cv setvar z
15 14 cuni class ⋃ z
16 6 15 wceq wff ⋃ x = ⋃ z
17 16 10 13 wrex wff ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
18 9 17 wi wff ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
19 18 3 5 wral wff ∀ y ∈ 𝒫 x ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
20 19 1 2 crab class x ∈ Top | ∀ y ∈ 𝒫 x ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z
21 0 20 wceq wff Comp = x ∈ Top | ∀ y ∈ 𝒫 x ⋃ x = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin ⋃ x = ⋃ z