MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-perf Unicode version

Definition df-perf 16885
Description: Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016.)
Assertion
Ref Expression
df-perf  |- Perf  =  {
j  e.  Top  | 
( ( limPt `  j
) `  U. j )  =  U. j }

Detailed syntax breakdown of Definition df-perf
StepHypRef Expression
1 cperf 16883 . 2  class Perf
2 vj . . . . . . 7  set  j
32cv 1631 . . . . . 6  class  j
43cuni 3843 . . . . 5  class  U. j
5 clp 16882 . . . . . 6  class  limPt
63, 5cfv 5271 . . . . 5  class  ( limPt `  j )
74, 6cfv 5271 . . . 4  class  ( (
limPt `  j ) `  U. j )
87, 4wceq 1632 . . 3  wff  ( (
limPt `  j ) `  U. j )  =  U. j
9 ctop 16647 . . 3  class  Top
108, 2, 9crab 2560 . 2  class  { j  e.  Top  |  ( ( limPt `  j ) `  U. j )  = 
U. j }
111, 10wceq 1632 1  wff Perf  =  {
j  e.  Top  | 
( ( limPt `  j
) `  U. j )  =  U. j }
Colors of variables: wff set class
This definition is referenced by:  isperf  16898
  Copyright terms: Public domain W3C validator