Theorem perfi

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

	Ref	Expression
Hypothesis	lpfval.1	$$⊢X=\bigcup J$$
Assertion	perfi	$$⊢\left(J\in \mathrm{Perf}\wedge P\in X\right)\to \neg \left\{P\right\}\in J$$

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$$⊢X=\bigcup J$$
2	1	isperf3	$$⊢J\in \mathrm{Perf}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in X\neg \left\{x\right\}\in J\right)$$
3	2	simprbi	$$⊢J\in \mathrm{Perf}\to \forall x\in X\neg \left\{x\right\}\in J$$
4		sneq	$$⊢x=P\to \left\{x\right\}=\left\{P\right\}$$
5	4	eleq1d	$$⊢x=P\to \left(\left\{x\right\}\in J\leftrightarrow \left\{P\right\}\in J\right)$$
6	5	notbid	$$⊢x=P\to \left(\neg \left\{x\right\}\in J\leftrightarrow \neg \left\{P\right\}\in J\right)$$
7	6	rspccva	$$⊢\left(\forall x\in X\neg \left\{x\right\}\in J\wedge P\in X\right)\to \neg \left\{P\right\}\in J$$
8	3 7	sylan	$$⊢\left(J\in \mathrm{Perf}\wedge P\in X\right)\to \neg \left\{P\right\}\in J$$