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 )