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