Metamath Proof Explorer


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 }