Theorem pibp16

Description: Property P000016 of pi-base. The class of compact topologies. A space X is compact if every open cover of X has a finite subcover. This theorem is just a relabeled copy of iscmp . (Contributed by ML, 8-Dec-2020)

	Ref	Expression
Hypothesis	pibp16.x	⊢ 𝑋 = ∪ 𝐽
Assertion	pibp16	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pibp16.x	⊢ 𝑋 = ∪ 𝐽
2	1	iscmp	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑋 = ∪ 𝑧 ) ) )