Definition df-cnrm 22467

Description: Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015.)

Assertion

Ref	Expression
df-cnrm	⊢ CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 ∪ 𝑗(𝑗 ↾t 𝑥) ∈ Nrm}

Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-cnrm

Step	Hyp	Ref	Expression
1		ccnrm 22460	. 2 class CNrm
2		vj	. . . . . . 7 setvar 𝑗
3	2	cv 1541	. . . . . 6 class 𝑗
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1541	. . . . . 6 class 𝑥
6		crest 17129	. . . . . 6 class ↾t
7	3, 5, 6	co 7271	. . . . 5 class (𝑗 ↾t 𝑥)
8		cnrm 22459	. . . . 5 class Nrm
9	7, 8	wcel 2110	. . . 4 wff (𝑗 ↾t 𝑥) ∈ Nrm
10	3	cuni 4845	. . . . 5 class ∪ 𝑗
11	10	cpw 4539	. . . 4 class 𝒫 ∪ 𝑗
12	9, 4, 11	wral 3066	. . 3 wff ∀𝑥 ∈ 𝒫 ∪ 𝑗(𝑗 ↾t 𝑥) ∈ Nrm
13		ctop 22040	. . 3 class Top
14	12, 2, 13	crab 3070	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 ∪ 𝑗(𝑗 ↾t 𝑥) ∈ Nrm}
15	1, 14	wceq 1542	1 wff CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 ∪ 𝑗(𝑗 ↾t 𝑥) ∈ Nrm}

This definition is referenced by:  iscnrm  22472