This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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