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 = ⋃ J
Assertion isperf3 ⊢ J ∈ Perf ↔ J ∈ Top ∧ ∀ x ∈ X ¬ x ∈ J

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 1 isperf2 ⊢ J ∈ Perf ↔ J ∈ Top ∧ X ⊆ limPt ⁡ J ⁡ X
3 dfss3 ⊢ X ⊆ limPt ⁡ J ⁡ X ↔ ∀ x ∈ X x ∈ limPt ⁡ J ⁡ X
4 1 maxlp ⊢ J ∈ Top → x ∈ limPt ⁡ J ⁡ X ↔ x ∈ X ∧ ¬ x ∈ J
5 4 baibd ⊢ J ∈ Top ∧ x ∈ X → x ∈ limPt ⁡ J ⁡ X ↔ ¬ x ∈ J
6 5 ralbidva ⊢ J ∈ Top → ∀ x ∈ X x ∈ limPt ⁡ J ⁡ X ↔ ∀ x ∈ X ¬ x ∈ J
7 3 6 syl5bb ⊢ J ∈ Top → X ⊆ limPt ⁡ J ⁡ X ↔ ∀ x ∈ X ¬ x ∈ J
8 7 pm5.32i ⊢ J ∈ Top ∧ X ⊆ limPt ⁡ J ⁡ X ↔ J ∈ Top ∧ ∀ x ∈ X ¬ x ∈ J
9 2 8 bitri ⊢ J ∈ Perf ↔ J ∈ Top ∧ ∀ x ∈ X ¬ x ∈ J