Database
BASIC TOPOLOGY
Topology
Limit points and perfect sets
isperf
Next ⟩
isperf2
Metamath Proof Explorer
Ascii
Unicode
Theorem
isperf
Description:
Definition of a perfect space.
(Contributed by
Mario Carneiro
, 24-Dec-2016)
Ref
Expression
Hypothesis
lpfval.1
⊢
X
=
⋃
J
Assertion
isperf
⊢
J
∈
Perf
↔
J
∈
Top
∧
limPt
⁡
J
⁡
X
=
X
Proof
Step
Hyp
Ref
Expression
1
lpfval.1
⊢
X
=
⋃
J
2
fveq2
⊢
j
=
J
→
limPt
⁡
j
=
limPt
⁡
J
3
unieq
⊢
j
=
J
→
⋃
j
=
⋃
J
4
3
1
eqtr4di
⊢
j
=
J
→
⋃
j
=
X
5
2
4
fveq12d
⊢
j
=
J
→
limPt
⁡
j
⁡
⋃
j
=
limPt
⁡
J
⁡
X
6
5
4
eqeq12d
⊢
j
=
J
→
limPt
⁡
j
⁡
⋃
j
=
⋃
j
↔
limPt
⁡
J
⁡
X
=
X
7
df-perf
⊢
Perf
=
j
∈
Top
|
limPt
⁡
j
⁡
⋃
j
=
⋃
j
8
6
7
elrab2
⊢
J
∈
Perf
↔
J
∈
Top
∧
limPt
⁡
J
⁡
X
=
X