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 = j Top | x 𝒫 j j 𝑡 x Nrm

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnrm class CNrm
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 4 cuni class j
6 5 cpw class 𝒫 j
7 crest class 𝑡
8 3 cv setvar x
9 4 8 7 co class j 𝑡 x
10 cnrm class Nrm
11 9 10 wcel wff j 𝑡 x Nrm
12 11 3 6 wral wff x 𝒫 j j 𝑡 x Nrm
13 12 1 2 crab class j Top | x 𝒫 j j 𝑡 x Nrm
14 0 13 wceq wff CNrm = j Top | x 𝒫 j j 𝑡 x Nrm