Theorem pibp19

Description: Property P000019 of pi-base. The class of countably compact topologies. A space X is countably compact if every countable open cover of X has a finite subcover. (Contributed by ML, 8-Dec-2020)

	Ref	Expression
Hypotheses	pibp19.x	|- X = U. J
	pibp19.19	|- C = { x e. Top | A. y e. ~P x ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
Assertion	pibp19	|- ( J e. C <-> ( J e. Top /\ A. y e. ~P J ( ( X = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )

Proof

Step	Hyp	Ref	Expression
1		pibp19.x	|- X = U. J
2		pibp19.19	|- C = { x e. Top | A. y e. ~P x ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) }
3		pweq	|- ( x = J -> ~P x = ~P J )
4		unieq	|- ( x = J -> U. x = U. J )
5	4 1	eqtr4di	|- ( x = J -> U. x = X )
6	5	eqeq1d	|- ( x = J -> ( U. x = U. y <-> X = U. y ) )
7	6	anbi1d	|- ( x = J -> ( ( U. x = U. y /\ y ~<_ _om ) <-> ( X = U. y /\ y ~<_ _om ) ) )
8	5	eqeq1d	|- ( x = J -> ( U. x = U. z <-> X = U. z ) )
9	8	rexbidv	|- ( x = J -> ( E. z e. ( ~P y i^i Fin ) U. x = U. z <-> E. z e. ( ~P y i^i Fin ) X = U. z ) )
10	7 9	imbi12d	|- ( x = J -> ( ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) <-> ( ( X = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
11	3 10	raleqbidv	|- ( x = J -> ( A. y e. ~P x ( ( U. x = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) U. x = U. z ) <-> A. y e. ~P J ( ( X = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )
12	11 2	elrab2	|- ( J e. C <-> ( J e. Top /\ A. y e. ~P J ( ( X = U. y /\ y ~<_ _om ) -> E. z e. ( ~P y i^i Fin ) X = U. z ) ) )