Theorem perfi

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

	Ref	Expression
Hypothesis	lpfval.1	|- X = U. J
Assertion	perfi	|- ( ( J e. Perf /\ P e. X ) -> -. { P } e. J )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	|- X = U. J
2	1	isperf3	|- ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )
3	2	simprbi	|- ( J e. Perf -> A. x e. X -. { x } e. J )
4		sneq	|- ( x = P -> { x } = { P } )
5	4	eleq1d	|- ( x = P -> ( { x } e. J <-> { P } e. J ) )
6	5	notbid	|- ( x = P -> ( -. { x } e. J <-> -. { P } e. J ) )
7	6	rspccva	|- ( ( A. x e. X -. { x } e. J /\ P e. X ) -> -. { P } e. J )
8	3 7	sylan	|- ( ( J e. Perf /\ P e. X ) -> -. { P } e. J )