Theorem isperf3

Description: A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$$⊢X=\bigcup J$$
2	1	isperf2	$$⊢J\in \mathrm{Perf}\leftrightarrow \left(J\in \mathrm{Top}\wedge X\subseteq \mathrm{limPt}\left(J\right)\left(X\right)\right)$$
3		dfss3	$$⊢X\subseteq \mathrm{limPt}\left(J\right)\left(X\right)\leftrightarrow \forall x\in Xx\in \mathrm{limPt}\left(J\right)\left(X\right)$$
4	1	maxlp	$$⊢J\in \mathrm{Top}\to \left(x\in \mathrm{limPt}\left(J\right)\left(X\right)\leftrightarrow \left(x\in X\wedge \neg \left\{x\right\}\in J\right)\right)$$
5	4	baibd	$$⊢\left(J\in \mathrm{Top}\wedge x\in X\right)\to \left(x\in \mathrm{limPt}\left(J\right)\left(X\right)\leftrightarrow \neg \left\{x\right\}\in J\right)$$
6	5	ralbidva	$$⊢J\in \mathrm{Top}\to \left(\forall x\in Xx\in \mathrm{limPt}\left(J\right)\left(X\right)\leftrightarrow \forall x\in X\neg \left\{x\right\}\in J\right)$$
7	3 6	bitrid	$$⊢J\in \mathrm{Top}\to \left(X\subseteq \mathrm{limPt}\left(J\right)\left(X\right)\leftrightarrow \forall x\in X\neg \left\{x\right\}\in J\right)$$
8	7	pm5.32i	$$⊢\left(J\in \mathrm{Top}\wedge X\subseteq \mathrm{limPt}\left(J\right)\left(X\right)\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in X\neg \left\{x\right\}\in J\right)$$
9	2 8	bitri	$$⊢J\in \mathrm{Perf}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in X\neg \left\{x\right\}\in J\right)$$