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 \in PNrm \land A \in Clsd (J)) \to \exists f \in (J^{ℕ}) A = ⋂ ran f$

Step	Hyp	Ref	Expression
1		ispnrm	$⊢ J \in PNrm \leftrightarrow (J \in Nrm \land Clsd (J) \subseteq ran (f \in (J^{ℕ}) ⟼ ⋂ ran f))$
2	1	simprbi	$⊢ J \in PNrm \to Clsd (J) \subseteq ran (f \in (J^{ℕ}) ⟼ ⋂ ran f)$
3	2	sselda	$⊢ (J \in PNrm \land A \in Clsd (J)) \to A \in ran (f \in (J^{ℕ}) ⟼ ⋂ ran f)$
4		eqid	$⊢ (f \in (J^{ℕ}) ⟼ ⋂ ran f) = (f \in (J^{ℕ}) ⟼ ⋂ ran f)$
5	4	elrnmpt	$⊢ A \in Clsd (J) \to (A \in ran (f \in (J^{ℕ}) ⟼ ⋂ ran f) \leftrightarrow \exists f \in (J^{ℕ}) A = ⋂ ran f)$
6	5	adantl	$⊢ (J \in PNrm \land A \in Clsd (J)) \to (A \in ran (f \in (J^{ℕ}) ⟼ ⋂ ran f) \leftrightarrow \exists f \in (J^{ℕ}) A = ⋂ ran f)$
7	3 6	mpbid	$⊢ (J \in PNrm \land A \in Clsd (J)) \to \exists f \in (J^{ℕ}) A = ⋂ ran f$

Metamath Proof Explorer