Theorem pibp21

Description: Property P000021 of pi-base. The class of weakly countably compact topologies, or limit point compact topologies. A space X is weakly countably compact if every infinite subset of X has a limit point. (Contributed by ML, 9-Dec-2020)

	Ref	Expression
Hypotheses	pibp21.x	|- X = U. J
	pibp21.21	|- W = { x e. Top | A. y e. ( ~P U. x \ Fin ) E. z e. U. x z e. ( ( limPt ` x ) ` y ) }
Assertion	pibp21	|- ( J e. W <-> ( J e. Top /\ A. y e. ( ~P X \ Fin ) E. z e. X z e. ( ( limPt ` J ) ` y ) ) )

Proof

Step	Hyp	Ref	Expression
1		pibp21.x	|- X = U. J
2		pibp21.21	|- W = { x e. Top | A. y e. ( ~P U. x \ Fin ) E. z e. U. x z e. ( ( limPt ` x ) ` y ) }
3		unieq	|- ( x = J -> U. x = U. J )
4	3 1	eqtr4di	|- ( x = J -> U. x = X )
5	4	pweqd	|- ( x = J -> ~P U. x = ~P X )
6	5	difeq1d	|- ( x = J -> ( ~P U. x \ Fin ) = ( ~P X \ Fin ) )
7		fveq2	|- ( x = J -> ( limPt ` x ) = ( limPt ` J ) )
8	7	fveq1d	|- ( x = J -> ( ( limPt ` x ) ` y ) = ( ( limPt ` J ) ` y ) )
9	8	eleq2d	|- ( x = J -> ( z e. ( ( limPt ` x ) ` y ) <-> z e. ( ( limPt ` J ) ` y ) ) )
10	4 9	rexeqbidv	|- ( x = J -> ( E. z e. U. x z e. ( ( limPt ` x ) ` y ) <-> E. z e. X z e. ( ( limPt ` J ) ` y ) ) )
11	6 10	raleqbidv	|- ( x = J -> ( A. y e. ( ~P U. x \ Fin ) E. z e. U. x z e. ( ( limPt ` x ) ` y ) <-> A. y e. ( ~P X \ Fin ) E. z e. X z e. ( ( limPt ` J ) ` y ) ) )
12	11 2	elrab2	|- ( J e. W <-> ( J e. Top /\ A. y e. ( ~P X \ Fin ) E. z e. X z e. ( ( limPt ` J ) ` y ) ) )