Definition df-pnrm 20933

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 = {𝑗 ∈ Nrm ∣ (Clsd‘𝑗) ⊆ ran (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)}

Distinct variable group:   𝑓,𝑗

Detailed syntax breakdown of Definition df-pnrm

Step	Hyp	Ref	Expression
1		cpnrm 20926	. 2 class PNrm
2		vj	. . . . . 6 setvar 𝑗
3	2	cv 1474	. . . . 5 class 𝑗
4		ccld 20630	. . . . 5 class Clsd
5	3, 4	cfv 5804	. . . 4 class (Clsd‘𝑗)
6		vf	. . . . . 6 setvar 𝑓
7		cn 10897	. . . . . . 7 class ℕ
8		cmap 7744	. . . . . . 7 class ↑𝑚
9	3, 7, 8	co 6549	. . . . . 6 class (𝑗 ↑𝑚 ℕ)
10	6	cv 1474	. . . . . . . 8 class 𝑓
11	10	crn 5039	. . . . . . 7 class ran 𝑓
12	11	cint 4410	. . . . . 6 class ∩ ran 𝑓
13	6, 9, 12	cmpt 4643	. . . . 5 class (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)
14	13	crn 5039	. . . 4 class ran (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)
15	5, 14	wss 3540	. . 3 wff (Clsd‘𝑗) ⊆ ran (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)
16		cnrm 20924	. . 3 class Nrm
17	15, 2, 16	crab 2900	. 2 class {𝑗 ∈ Nrm ∣ (Clsd‘𝑗) ⊆ ran (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)}
18	1, 17	wceq 1475	1 wff PNrm = {𝑗 ∈ Nrm ∣ (Clsd‘𝑗) ⊆ ran (𝑓 ∈ (𝑗 ↑𝑚 ℕ) ↦ ∩ ran 𝑓)}

This definition is referenced by:  ispnrm  20953