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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpnrm	⊢ PNrm
1		vj	⊢ 𝑗
2		cnrm	⊢ Nrm
3		ccld	⊢ Clsd
4	1	cv	⊢ 𝑗
5	4 3	cfv	⊢ ( Clsd ‘ 𝑗 )
6		vf	⊢ 𝑓
7		cmap	⊢ ↑m
8		cn	⊢ ℕ
9	4 8 7	co	⊢ ( 𝑗 ↑m ℕ )
10	6	cv	⊢ 𝑓
11	10	crn	⊢ ran 𝑓
12	11	cint	⊢ ∩ ran 𝑓
13	6 9 12	cmpt	⊢ ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 )
14	13	crn	⊢ ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 )
15	5 14	wss	⊢ ( Clsd ‘ 𝑗 ) ⊆ ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 )
16	15 1 2	crab	⊢ { 𝑗 ∈ Nrm ∣ ( Clsd ‘ 𝑗 ) ⊆ ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 ) }
17	0 16	wceq	⊢ PNrm = { 𝑗 ∈ Nrm ∣ ( Clsd ‘ 𝑗 ) ⊆ ran ( 𝑓 ∈ ( 𝑗 ↑m ℕ ) ↦ ∩ ran 𝑓 ) }