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 ) ∪ 𝑥 = ∪ 𝑧 ) }