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 = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmp ⊢ Comp
1 vx ⊢ 𝑥
2 ctop ⊢ Top
3 vy ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 4 cpw ⊢ 𝒫 𝑥
6 4 cuni ⊢ ∪ 𝑥
7 3 cv ⊢ 𝑦
8 7 cuni ⊢ ∪ 𝑦
9 6 8 wceq ⊢ ∪ 𝑥 = ∪ 𝑦
10 vz ⊢ 𝑧
11 7 cpw ⊢ 𝒫 𝑦
12 cfn ⊢ Fin
13 11 12 cin ⊢ ( 𝒫 𝑦 ∩ Fin )
14 10 cv ⊢ 𝑧
15 14 cuni ⊢ ∪ 𝑧
16 6 15 wceq ⊢ ∪ 𝑥 = ∪ 𝑧
17 16 10 13 wrex ⊢ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧
18 9 17 wi ⊢ ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 )
19 18 3 5 wral ⊢ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 )
20 19 1 2 crab ⊢ { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }
21 0 20 wceq ⊢ Comp = { 𝑥 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( ∪ 𝑥 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝑥 = ∪ 𝑧 ) }