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 = { 𝑗 ∈ 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 𝑓 ) }