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

Definition df-perf 22641
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 = {𝑗 ∈ Top ∣ ((limPtβ€˜π‘—)β€˜βˆͺ 𝑗) = βˆͺ 𝑗}

Detailed syntax breakdown of Definition df-perf
StepHypRef Expression
1 cperf 22639 . 2 class Perf
2 vj . . . . . . 7 setvar 𝑗
32cv 1541 . . . . . 6 class 𝑗
43cuni 4909 . . . . 5 class βˆͺ 𝑗
5 clp 22638 . . . . . 6 class limPt
63, 5cfv 6544 . . . . 5 class (limPtβ€˜π‘—)
74, 6cfv 6544 . . . 4 class ((limPtβ€˜π‘—)β€˜βˆͺ 𝑗)
87, 4wceq 1542 . . 3 wff ((limPtβ€˜π‘—)β€˜βˆͺ 𝑗) = βˆͺ 𝑗
9 ctop 22395 . . 3 class Top
108, 2, 9crab 3433 . 2 class {𝑗 ∈ Top ∣ ((limPtβ€˜π‘—)β€˜βˆͺ 𝑗) = βˆͺ 𝑗}
111, 10wceq 1542 1 wff Perf = {𝑗 ∈ Top ∣ ((limPtβ€˜π‘—)β€˜βˆͺ 𝑗) = βˆͺ 𝑗}
Colors of variables: wff setvar class
This definition is referenced by:  isperf  22655
  Copyright terms: Public domain W3C validator