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

Metamath Proof Explorer

Theorem kqtop

Description: The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion kqtop 
|- ( J e. Top <-> ( KQ ` J ) e. Top )

Proof

Step Hyp Ref Expression
1 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
2 eqid 
 |-  ( x e. U. J |-> { y e. J | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } )
3 2 kqtopon 
 |-  ( J e. ( TopOn ` U. J ) -> ( KQ ` J ) e. ( TopOn ` ran ( x e. U. J |-> { y e. J | x e. y } ) ) )
4 1 3 sylbi 
 |-  ( J e. Top -> ( KQ ` J ) e. ( TopOn ` ran ( x e. U. J |-> { y e. J | x e. y } ) ) )
5 topontop 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran ( x e. U. J |-> { y e. J | x e. y } ) ) -> ( KQ ` J ) e. Top )
6 4 5 syl 
 |-  ( J e. Top -> ( KQ ` J ) e. Top )
7 0opn 
 |-  ( ( KQ ` J ) e. Top -> (/) e. ( KQ ` J ) )
8 elfvdm 
 |-  ( (/) e. ( KQ ` J ) -> J e. dom KQ )
9 7 8 syl 
 |-  ( ( KQ ` J ) e. Top -> J e. dom KQ )
10 ovex 
 |-  ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) e. _V
11 df-kq 
 |-  KQ = ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) )
12 10 11 dmmpti 
 |-  dom KQ = Top
13 9 12 eleqtrdi 
 |-  ( ( KQ ` J ) e. Top -> J e. Top )
14 6 13 impbii 
 |-  ( J e. Top <-> ( KQ ` J ) e. Top )