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	|- PNrm = { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpnrm	|- PNrm
1		vj	|- j
2		cnrm	|- Nrm
3		ccld	|- Clsd
4	1	cv	|- j
5	4 3	cfv	|- ( Clsd ` j )
6		vf	|- f
7		cmap	|- ^m
8		cn	|- NN
9	4 8 7	co	|- ( j ^m NN )
10	6	cv	|- f
11	10	crn	|- ran f
12	11	cint	|- |^| ran f
13	6 9 12	cmpt	|- ( f e. ( j ^m NN ) |-> |^| ran f )
14	13	crn	|- ran ( f e. ( j ^m NN ) |-> |^| ran f )
15	5 14	wss	|- ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f )
16	15 1 2	crab	|- { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }
17	0 16	wceq	|- PNrm = { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }