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	$$⊢X=\bigcup J$$
Assertion	pibp16	$$⊢J\in \mathrm{Comp}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pibp16.x	$$⊢X=\bigcup J$$
2	1	iscmp	$$⊢J\in \mathrm{Comp}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall y\in 𝒫J\left(X=\bigcup y\to \exists z\in \left(𝒫y\cap \mathrm{Fin}\right)X=\bigcup z\right)\right)$$