Metamath Proof Explorer

Theorem kqnrm

Description: The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqnrm 
|- ( J e. Nrm <-> ( KQ ` J ) e. Nrm )

Proof

Step Hyp Ref Expression
1 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
2 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
3 1 2 sylib 
 |-  ( J e. Nrm -> 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 kqnrmlem1 
 |-  ( ( J e. ( TopOn ` U. J ) /\ J e. Nrm ) -> ( KQ ` J ) e. Nrm )
6 3 5 mpancom 
 |-  ( J e. Nrm -> ( KQ ` J ) e. Nrm )
7 nrmtop 
 |-  ( ( KQ ` J ) e. Nrm -> ( KQ ` J ) e. Top )
8 kqtop 
 |-  ( J e. Top <-> ( KQ ` J ) e. Top )
9 7 8 sylibr 
 |-  ( ( KQ ` J ) e. Nrm -> J e. Top )
10 9 2 sylib 
 |-  ( ( KQ ` J ) e. Nrm -> J e. ( TopOn ` U. J ) )
11 4 kqnrmlem2 
 |-  ( ( J e. ( TopOn ` U. J ) /\ ( KQ ` J ) e. Nrm ) -> J e. Nrm )
12 10 11 mpancom 
 |-  ( ( KQ ` J ) e. Nrm -> J e. Nrm )
13 6 12 impbii 
 |-  ( J e. Nrm <-> ( KQ ` J ) e. Nrm )