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 22469
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 22462 . 2 class CNrm
2 vj . . . . . . 7 setvar 𝑗
32cv 1538 . . . . . 6 class 𝑗
4 vx . . . . . . 7 setvar 𝑥
54cv 1538 . . . . . 6 class 𝑥
6 crest 17131 . . . . . 6 class t
73, 5, 6co 7275 . . . . 5 class (𝑗t 𝑥)
8 cnrm 22461 . . . . 5 class Nrm
97, 8wcel 2106 . . . 4 wff (𝑗t 𝑥) ∈ Nrm
103cuni 4839 . . . . 5 class 𝑗
1110cpw 4533 . . . 4 class 𝒫 𝑗
129, 4, 11wral 3064 . . 3 wff 𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm
13 ctop 22042 . . 3 class Top
1412, 2, 13crab 3068 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
151, 14wceq 1539 1 wff CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
Colors of variables: wff setvar class
This definition is referenced by:  iscnrm  22474
  Copyright terms: Public domain W3C validator