This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ Nrm | Clsd ⁡ j ⊆ ran ⁡ f ∈ j ℕ ⟼ ⋂ ran ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpnrm class PNrm
1 vj setvar j
2 cnrm class Nrm
3 ccld class Clsd
4 1 cv setvar j
5 4 3 cfv class Clsd ⁡ j
6 vf setvar f
7 cmap class ↑ 𝑚
8 cn class ℕ
9 4 8 7 co class j ℕ
10 6 cv setvar f
11 10 crn class ran ⁡ f
12 11 cint class ⋂ ran ⁡ f
13 6 9 12 cmpt class f ∈ j ℕ ⟼ ⋂ ran ⁡ f
14 13 crn class ran ⁡ f ∈ j ℕ ⟼ ⋂ ran ⁡ f
15 5 14 wss wff Clsd ⁡ j ⊆ ran ⁡ f ∈ j ℕ ⟼ ⋂ ran ⁡ f
16 15 1 2 crab class j ∈ Nrm | Clsd ⁡ j ⊆ ran ⁡ f ∈ j ℕ ⟼ ⋂ ran ⁡ f
17 0 16 wceq wff PNrm = j ∈ Nrm | Clsd ⁡ j ⊆ ran ⁡ f ∈ j ℕ ⟼ ⋂ ran ⁡ f