Metamath Proof Explorer


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 syl5bb
 |-  ( 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 ) )