This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ∃ 𝑓 ∈ ( 𝐽 ↑m ℕ ) 𝐴 = ∩ ran 𝑓 )

Proof

Step Hyp Ref Expression
1 ispnrm ⊢ ( 𝐽 ∈ PNrm ↔ ( 𝐽 ∈ Nrm ∧ ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ) )
2 1 simprbi ⊢ ( 𝐽 ∈ PNrm → ( Clsd ‘ 𝐽 ) ⊆ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) )
3 2 sselda ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐴 ∈ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) )
4 eqid ⊢ ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) = ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 )
5 4 elrnmpt ⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐴 ∈ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ↔ ∃ 𝑓 ∈ ( 𝐽 ↑m ℕ ) 𝐴 = ∩ ran 𝑓 ) )
6 5 adantl ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐴 ∈ ran ( 𝑓 ∈ ( 𝐽 ↑m ℕ ) ↦ ∩ ran 𝑓 ) ↔ ∃ 𝑓 ∈ ( 𝐽 ↑m ℕ ) 𝐴 = ∩ ran 𝑓 ) )
7 3 6 mpbid ⊢ ( ( 𝐽 ∈ PNrm ∧ 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) → ∃ 𝑓 ∈ ( 𝐽 ↑m ℕ ) 𝐴 = ∩ ran 𝑓 )