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

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 ( 𝐽 ∈ Reg ↔ ( KQ ‘ 𝐽 ) ∈ Reg )

Proof

Step Hyp Ref Expression
1 regtop ⊢ ( 𝐽 ∈ Reg → 𝐽 ∈ Top )
2 toptopon2 ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
3 1 2 sylib ⊢ ( 𝐽 ∈ Reg → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
4 eqid ⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
5 4 kqreglem1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Reg )
6 3 5 mpancom ⊢ ( 𝐽 ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Reg )
7 regtop ⊢ ( ( KQ ‘ 𝐽 ) ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Top )
8 kqtop ⊢ ( 𝐽 ∈ Top ↔ ( KQ ‘ 𝐽 ) ∈ Top )
9 7 8 sylibr ⊢ ( ( KQ ‘ 𝐽 ) ∈ Reg → 𝐽 ∈ Top )
10 9 2 sylib ⊢ ( ( KQ ‘ 𝐽 ) ∈ Reg → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
11 4 kqreglem2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( KQ ‘ 𝐽 ) ∈ Reg ) → 𝐽 ∈ Reg )
12 10 11 mpancom ⊢ ( ( KQ ‘ 𝐽 ) ∈ Reg → 𝐽 ∈ Reg )
13 6 12 impbii ⊢ ( 𝐽 ∈ Reg ↔ ( KQ ‘ 𝐽 ) ∈ Reg )