Definition df-pnrm 21123

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.)

Assertion

Ref	Expression
df-pnrm	|- PNrm = { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }

Distinct variable group:   f, j

Detailed syntax breakdown of Definition df-pnrm

Step	Hyp	Ref	Expression
1		cpnrm 21116	. 2 class PNrm
2		vj	. . . . . 6 setvar j
3	2	cv 1482	. . . . 5 class j
4		ccld 20820	. . . . 5 class Clsd
5	3, 4	cfv 5888	. . . 4 class ( Clsd ` j )
6		vf	. . . . . 6 setvar f
7		cn 11020	. . . . . . 7 class NN
8		cmap 7857	. . . . . . 7 class ^m
9	3, 7, 8	co 6650	. . . . . 6 class ( j ^m NN )
10	6	cv 1482	. . . . . . . 8 class f
11	10	crn 5115	. . . . . . 7 class ran f
12	11	cint 4475	. . . . . 6 class |^| ran f
13	6, 9, 12	cmpt 4729	. . . . 5 class ( f e. ( j ^m NN ) |-> |^| ran f )
14	13	crn 5115	. . . 4 class ran ( f e. ( j ^m NN ) |-> |^| ran f )
15	5, 14	wss 3574	. . 3 wff ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f )
16		cnrm 21114	. . 3 class Nrm
17	15, 2, 16	crab 2916	. 2 class { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }
18	1, 17	wceq 1483	1 wff PNrm = { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }

This definition is referenced by:  ispnrm  21143