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 22467
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 22460 . 2 class CNrm
2 vj . . . . . . 7 setvar 𝑗
32cv 1541 . . . . . 6 class 𝑗
4 vx . . . . . . 7 setvar 𝑥
54cv 1541 . . . . . 6 class 𝑥
6 crest 17129 . . . . . 6 class t
73, 5, 6co 7271 . . . . 5 class (𝑗t 𝑥)
8 cnrm 22459 . . . . 5 class Nrm
97, 8wcel 2110 . . . 4 wff (𝑗t 𝑥) ∈ Nrm
103cuni 4845 . . . . 5 class 𝑗
1110cpw 4539 . . . 4 class 𝒫 𝑗
129, 4, 11wral 3066 . . 3 wff 𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm
13 ctop 22040 . . 3 class Top
1412, 2, 13crab 3070 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
151, 14wceq 1542 1 wff CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
Colors of variables: wff setvar class
This definition is referenced by:  iscnrm  22472
  Copyright terms: Public domain W3C validator