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

Metamath Proof Explorer

Theorem kqval

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion kqval 
|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
3 id 
 |-  ( j = J -> j = J )
4 unieq 
 |-  ( j = J -> U. j = U. J )
5 rabeq 
 |-  ( j = J -> { y e. j | x e. y } = { y e. J | x e. y } )
6 4 5 mpteq12dv 
 |-  ( j = J -> ( x e. U. j |-> { y e. j | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } ) )
7 3 6 oveq12d 
 |-  ( j = J -> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) = ( J qTop ( x e. U. J |-> { y e. J | x e. y } ) ) )
8 df-kq 
 |-  KQ = ( j e. Top |-> ( j qTop ( x e. U. j |-> { y e. j | x e. y } ) ) )
9 ovex 
 |-  ( J qTop ( x e. U. J |-> { y e. J | x e. y } ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( J e. Top -> ( KQ ` J ) = ( J qTop ( x e. U. J |-> { y e. J | x e. y } ) ) )
11 2 10 syl 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop ( x e. U. J |-> { y e. J | x e. y } ) ) )
12 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
13 12 mpteq1d 
 |-  ( J e. ( TopOn ` X ) -> ( x e. X |-> { y e. J | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } ) )
14 1 13 eqtrid 
 |-  ( J e. ( TopOn ` X ) -> F = ( x e. U. J |-> { y e. J | x e. y } ) )
15 14 oveq2d 
 |-  ( J e. ( TopOn ` X ) -> ( J qTop F ) = ( J qTop ( x e. U. J |-> { y e. J | x e. y } ) ) )
16 11 15 eqtr4d 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) )