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 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm }
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
ccnrm
⊢ CNrm
1
vj
⊢ 𝑗
2
ctop
⊢ Top
3
vx
⊢ 𝑥
4
1
cv
⊢ 𝑗
5
4
cuni
⊢ ∪ 𝑗
6
5
cpw
⊢ 𝒫 ∪ 𝑗
7
crest
⊢ ↾t
8
3
cv
⊢ 𝑥
9
4 8 7
co
⊢ ( 𝑗 ↾t 𝑥 )
10
cnrm
⊢ Nrm
11
9 10
wcel
⊢ ( 𝑗 ↾t 𝑥 ) ∈ Nrm
12
11 3 6
wral
⊢ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm
13
12 1 2
crab
⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm }
14
0 13
wceq
⊢ CNrm = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝒫 ∪ 𝑗 ( 𝑗 ↾t 𝑥 ) ∈ Nrm }