Metamath Proof Explorer

Theorem kqreg

Description: The Kolmogorov quotient of a regular space is regular. By regr1 it is also Hausdorff, so we can also say that a space is regular iff the Kolmogorov quotient is regular Hausdorff (T_3). (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqreg ⊢ J ∈ Reg ↔ KQ ⁡ J ∈ Reg

Proof

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