This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cnrm

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 }