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 = U. J
Assertion	isperf3	|- ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	|- X = U. J
2	1	isperf2	|- ( J e. Perf <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) )
3		dfss3	|- ( X C_ ( ( limPt ` J ) ` X ) <-> A. x e. X x e. ( ( limPt ` J ) ` X ) )
4	1	maxlp	|- ( J e. Top -> ( x e. ( ( limPt ` J ) ` X ) <-> ( x e. X /\ -. { x } e. J ) ) )
5	4	baibd	|- ( ( J e. Top /\ x e. X ) -> ( x e. ( ( limPt ` J ) ` X ) <-> -. { x } e. J ) )
6	5	ralbidva	|- ( J e. Top -> ( A. x e. X x e. ( ( limPt ` J ) ` X ) <-> A. x e. X -. { x } e. J ) )
7	3 6	bitrid	|- ( J e. Top -> ( X C_ ( ( limPt ` J ) ` X ) <-> A. x e. X -. { x } e. J ) )
8	7	pm5.32i	|- ( ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )
9	2 8	bitri	|- ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )