Definition df-cnrm

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnrm	⊢ CNrm
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6	5	cpw	⊢ 𝒫 ∪ 𝑗
7		crest	⊢ ↾t
8	3	cv	⊢ 𝑥
9	4 8 7	co	⊢ ( 𝑗 ↾t 𝑥 )
10		cnrm	⊢ Nrm
11	9 10	wcel	⊢ ( 𝑗 ↾t 𝑥 ) ∈ Nrm
12	11 3 6	wral	⊢ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm
13	12 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm }
14	0 13	wceq	⊢ CNrm = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm }