MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnrm Structured version   Visualization version   GIF version

Definition df-cnrm 21342
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
StepHypRef Expression
1 ccnrm 21335 . 2 class CNrm
2 vj . . . . . . 7 setvar 𝑗
32cv 1629 . . . . . 6 class 𝑗
4 vx . . . . . . 7 setvar 𝑥
54cv 1629 . . . . . 6 class 𝑥
6 crest 16288 . . . . . 6 class t
73, 5, 6co 6792 . . . . 5 class (𝑗t 𝑥)
8 cnrm 21334 . . . . 5 class Nrm
97, 8wcel 2144 . . . 4 wff (𝑗t 𝑥) ∈ Nrm
103cuni 4572 . . . . 5 class 𝑗
1110cpw 4295 . . . 4 class 𝒫 𝑗
129, 4, 11wral 3060 . . 3 wff 𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm
13 ctop 20917 . . 3 class Top
1412, 2, 13crab 3064 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
151, 14wceq 1630 1 wff CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
Colors of variables: wff setvar class
This definition is referenced by:  iscnrm  21347
  Copyright terms: Public domain W3C validator