Theorem isperf

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

	Ref	Expression
Hypothesis	lpfval.1	$$⊢X=\bigcup J$$
Assertion	isperf	$$⊢J\in \mathrm{Perf}\leftrightarrow \left(J\in \mathrm{Top}\wedge \mathrm{limPt}\left(J\right)\left(X\right)=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$$⊢X=\bigcup J$$
2		fveq2	$$⊢j=J\to \mathrm{limPt}\left(j\right)=\mathrm{limPt}\left(J\right)$$
3		unieq	$$⊢j=J\to \bigcup j=\bigcup J$$
4	3 1	eqtr4di	$$⊢j=J\to \bigcup j=X$$
5	2 4	fveq12d	$$⊢j=J\to \mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\mathrm{limPt}\left(J\right)\left(X\right)$$
6	5 4	eqeq12d	$$⊢j=J\to \left(\mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\bigcup j\leftrightarrow \mathrm{limPt}\left(J\right)\left(X\right)=X\right)$$
7		df-perf	$$⊢\mathrm{Perf}=\left\{j\in \mathrm{Top}|\mathrm{limPt}\left(j\right)\left(\bigcup j\right)=\bigcup j\right\}$$
8	6 7	elrab2	$$⊢J\in \mathrm{Perf}\leftrightarrow \left(J\in \mathrm{Top}\wedge \mathrm{limPt}\left(J\right)\left(X\right)=X\right)$$