Metamath Proof Explorer

Theorem isperf2

Description: Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis lpfval.1 ⊢ X = ⋃ J
Assertion isperf2 ⊢ J ∈ Perf ↔ J ∈ Top ∧ X ⊆ limPt ⁡ J ⁡ X

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 1 isperf ⊢ J ∈ Perf ↔ J ∈ Top ∧ limPt ⁡ J ⁡ X = X
3 ssid ⊢ X ⊆ X
4 1 lpss ⊢ J ∈ Top ∧ X ⊆ X → limPt ⁡ J ⁡ X ⊆ X
5 3 4 mpan2 ⊢ J ∈ Top → limPt ⁡ J ⁡ X ⊆ X
6 eqss ⊢ limPt ⁡ J ⁡ X = X ↔ limPt ⁡ J ⁡ X ⊆ X ∧ X ⊆ limPt ⁡ J ⁡ X
7 6 baib ⊢ limPt ⁡ J ⁡ X ⊆ X → limPt ⁡ J ⁡ X = X ↔ X ⊆ limPt ⁡ J ⁡ X
8 5 7 syl ⊢ J ∈ Top → limPt ⁡ J ⁡ X = X ↔ X ⊆ limPt ⁡ J ⁡ X
9 8 pm5.32i ⊢ J ∈ Top ∧ limPt ⁡ J ⁡ X = X ↔ J ∈ Top ∧ X ⊆ limPt ⁡ J ⁡ X
10 2 9 bitri ⊢ J ∈ Perf ↔ J ∈ Top ∧ X ⊆ limPt ⁡ J ⁡ X