Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-perf | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-perf | ⊢ Perf = {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cperf 22284 | . 2 class Perf | |
2 | vj | . . . . . . 7 setvar 𝑗 | |
3 | 2 | cv 1541 | . . . . . 6 class 𝑗 |
4 | 3 | cuni 4845 | . . . . 5 class ∪ 𝑗 |
5 | clp 22283 | . . . . . 6 class limPt | |
6 | 3, 5 | cfv 6432 | . . . . 5 class (limPt‘𝑗) |
7 | 4, 6 | cfv 6432 | . . . 4 class ((limPt‘𝑗)‘∪ 𝑗) |
8 | 7, 4 | wceq 1542 | . . 3 wff ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗 |
9 | ctop 22040 | . . 3 class Top | |
10 | 8, 2, 9 | crab 3070 | . 2 class {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗} |
11 | 1, 10 | wceq 1542 | 1 wff Perf = {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗} |
Colors of variables: wff setvar class |
This definition is referenced by: isperf 22300 |
Copyright terms: Public domain | W3C validator |