Theorem isperf

Description: Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	lpfval.1	|- X = U. J
Assertion	isperf	|- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	|- X = U. J
2		fveq2	|- ( j = J -> ( limPt ` j ) = ( limPt ` J ) )
3		unieq	|- ( j = J -> U. j = U. J )
4	3 1	eqtr4di	|- ( j = J -> U. j = X )
5	2 4	fveq12d	|- ( j = J -> ( ( limPt ` j ) ` U. j ) = ( ( limPt ` J ) ` X ) )
6	5 4	eqeq12d	|- ( j = J -> ( ( ( limPt ` j ) ` U. j ) = U. j <-> ( ( limPt ` J ) ` X ) = X ) )
7		df-perf	|- Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }
8	6 7	elrab2	|- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) )