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 = U. J |
|
| Assertion | pibp16 | |- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pibp16.x | |- X = U. J |
|
| 2 | 1 | iscmp | |- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( X = U. y -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) ) |