Definition df-pnrm

Description: Define perfectly normal spaces. A space is perfectly normal if it is normal and every closed set is a G_δ set, meaning that it is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	df-pnrm	$$⊢\mathrm{PNrm}=\left\{j\in \mathrm{Nrm}|\mathrm{Clsd}\left(j\right)\subseteq \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpnrm	$$class\mathrm{PNrm}$$
1		vj	$$setvarj$$
2		cnrm	$$class\mathrm{Nrm}$$
3		ccld	$$class\mathrm{Clsd}$$
4	1	cv	$$setvarj$$
5	4 3	cfv	$$class\mathrm{Clsd}\left(j\right)$$
6		vf	$$setvarf$$
7		cmap	$$class{\uparrow }_{𝑚}$$
8		cn	$$class\mathbb{N}$$
9	4 8 7	co	$$class\left(j^{\mathbb{N}}\right)$$
10	6	cv	$$setvarf$$
11	10	crn	$$class\mathrm{ran}f$$
12	11	cint	$$class\bigcap \mathrm{ran}f$$
13	6 9 12	cmpt	$$class\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)$$
14	13	crn	$$class\mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)$$
15	5 14	wss	$$wff\mathrm{Clsd}\left(j\right)\subseteq \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)$$
16	15 1 2	crab	$$class\left\{j\in \mathrm{Nrm}|\mathrm{Clsd}\left(j\right)\subseteq \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right\}$$
17	0 16	wceq	$$wff\mathrm{PNrm}=\left\{j\in \mathrm{Nrm}|\mathrm{Clsd}\left(j\right)\subseteq \mathrm{ran}\left(f\in \left(j^{\mathbb{N}}\right)⟼\bigcap \mathrm{ran}f\right)\right\}$$