Theorem kqffn

Description: The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion	kqffn	|- ( J e. V -> F Fn X )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
2		ssrab2	|- { y e. J | x e. y } C_ J
3		elpw2g	|- ( J e. V -> ( { y e. J | x e. y } e. ~P J <-> { y e. J | x e. y } C_ J ) )
4	2 3	mpbiri	|- ( J e. V -> { y e. J | x e. y } e. ~P J )
5	4	adantr	|- ( ( J e. V /\ x e. X ) -> { y e. J | x e. y } e. ~P J )
6	5 1	fmptd	|- ( J e. V -> F : X --> ~P J )
7	6	ffnd	|- ( J e. V -> F Fn X )