Metamath Proof Explorer

Theorem pnrmcld

Description: A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion pnrmcld ⊢ J ∈ PNrm ∧ A ∈ Clsd ⁡ J → ∃ f ∈ J ℕ A = ⋂ ran ⁡ f

Proof

Step Hyp Ref Expression
1 ispnrm ⊢ J ∈ PNrm ↔ J ∈ Nrm ∧ Clsd ⁡ J ⊆ ran ⁡ f ∈ J ℕ ⟼ ⋂ ran ⁡ f
2 1 simprbi ⊢ J ∈ PNrm → Clsd ⁡ J ⊆ ran ⁡ f ∈ J ℕ ⟼ ⋂ ran ⁡ f
3 2 sselda ⊢ J ∈ PNrm ∧ A ∈ Clsd ⁡ J → A ∈ ran ⁡ f ∈ J ℕ ⟼ ⋂ ran ⁡ f
4 eqid ⊢ f ∈ J ℕ ⟼ ⋂ ran ⁡ f = f ∈ J ℕ ⟼ ⋂ ran ⁡ f
5 4 elrnmpt ⊢ A ∈ Clsd ⁡ J → A ∈ ran ⁡ f ∈ J ℕ ⟼ ⋂ ran ⁡ f ↔ ∃ f ∈ J ℕ A = ⋂ ran ⁡ f
6 5 adantl ⊢ J ∈ PNrm ∧ A ∈ Clsd ⁡ J → A ∈ ran ⁡ f ∈ J ℕ ⟼ ⋂ ran ⁡ f ↔ ∃ f ∈ J ℕ A = ⋂ ran ⁡ f
7 3 6 mpbid ⊢ J ∈ PNrm ∧ A ∈ Clsd ⁡ J → ∃ f ∈ J ℕ A = ⋂ ran ⁡ f