Metamath Proof Explorer

Theorem kqnrm

Description: The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqnrm ⊢ J ∈ Nrm ↔ KQ ⁡ J ∈ Nrm

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ J ∈ Nrm → J ∈ Top
2 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylib ⊢ J ∈ Nrm → J ∈ TopOn ⁡ ⋃ J
4 eqid ⊢ x ∈ ⋃ J ⟼ y ∈ J | x ∈ y = x ∈ ⋃ J ⟼ y ∈ J | x ∈ y
5 4 kqnrmlem1 ⊢ J ∈ TopOn ⁡ ⋃ J ∧ J ∈ Nrm → KQ ⁡ J ∈ Nrm
6 3 5 mpancom ⊢ J ∈ Nrm → KQ ⁡ J ∈ Nrm
7 nrmtop ⊢ KQ ⁡ J ∈ Nrm → KQ ⁡ J ∈ Top
8 kqtop ⊢ J ∈ Top ↔ KQ ⁡ J ∈ Top
9 7 8 sylibr ⊢ KQ ⁡ J ∈ Nrm → J ∈ Top
10 9 2 sylib ⊢ KQ ⁡ J ∈ Nrm → J ∈ TopOn ⁡ ⋃ J
11 4 kqnrmlem2 ⊢ J ∈ TopOn ⁡ ⋃ J ∧ KQ ⁡ J ∈ Nrm → J ∈ Nrm
12 10 11 mpancom ⊢ KQ ⁡ J ∈ Nrm → J ∈ Nrm
13 6 12 impbii ⊢ J ∈ Nrm ↔ KQ ⁡ J ∈ Nrm