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