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 e. Reg <-> ( KQ ` J ) e. Reg )

Proof

Step	Hyp	Ref	Expression
1		regtop	|- ( J e. Reg -> J e. Top )
2		toptopon2	|- ( J e. Top <-> J e. ( TopOn ` U. J ) )
3	1 2	sylib	|- ( J e. Reg -> J e. ( TopOn ` U. J ) )
4		eqid	|- ( x e. U. J |-> { y e. J | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } )
5	4	kqreglem1	|- ( ( J e. ( TopOn ` U. J ) /\ J e. Reg ) -> ( KQ ` J ) e. Reg )
6	3 5	mpancom	|- ( J e. Reg -> ( KQ ` J ) e. Reg )
7		regtop	|- ( ( KQ ` J ) e. Reg -> ( KQ ` J ) e. Top )
8		kqtop	|- ( J e. Top <-> ( KQ ` J ) e. Top )
9	7 8	sylibr	|- ( ( KQ ` J ) e. Reg -> J e. Top )
10	9 2	sylib	|- ( ( KQ ` J ) e. Reg -> J e. ( TopOn ` U. J ) )
11	4	kqreglem2	|- ( ( J e. ( TopOn ` U. J ) /\ ( KQ ` J ) e. Reg ) -> J e. Reg )
12	10 11	mpancom	|- ( ( KQ ` J ) e. Reg -> J e. Reg )
13	6 12	impbii	|- ( J e. Reg <-> ( KQ ` J ) e. Reg )