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 
|- ( 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 )