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

Definition df-cnrm 20932
 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 20925 . 2 class CNrm
2 vj . . . . . . 7 setvar 𝑗
32cv 1474 . . . . . 6 class 𝑗
4 vx . . . . . . 7 setvar 𝑥
54cv 1474 . . . . . 6 class 𝑥
6 crest 15904 . . . . . 6 class t
73, 5, 6co 6549 . . . . 5 class (𝑗t 𝑥)
8 cnrm 20924 . . . . 5 class Nrm
97, 8wcel 1977 . . . 4 wff (𝑗t 𝑥) ∈ Nrm
103cuni 4372 . . . . 5 class 𝑗
1110cpw 4108 . . . 4 class 𝒫 𝑗
129, 4, 11wral 2896 . . 3 wff 𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm
13 ctop 20517 . . 3 class Top
1412, 2, 13crab 2900 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
151, 14wceq 1475 1 wff CNrm = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝒫 𝑗(𝑗t 𝑥) ∈ Nrm}
 Colors of variables: wff setvar class This definition is referenced by:  iscnrm  20937
 Copyright terms: Public domain W3C validator