Database
BASIC TOPOLOGY
Topology
Separated spaces: T0, T1, T2 (Hausdorff) ...
df-cnrm
Metamath Proof Explorer
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