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=\left(x\in X⟼\left\{y\in J|x\in y\right\}\right)$$
Assertion	kqffn	$$⊢J\in V\to FFnX$$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$$⊢F=\left(x\in X⟼\left\{y\in J|x\in y\right\}\right)$$
2		ssrab2	$$⊢\left\{y\in J|x\in y\right\}\subseteq J$$
3		elpw2g	$$⊢J\in V\to \left(\left\{y\in J|x\in y\right\}\in 𝒫J\leftrightarrow \left\{y\in J|x\in y\right\}\subseteq J\right)$$
4	2 3	mpbiri	$$⊢J\in V\to \left\{y\in J|x\in y\right\}\in 𝒫J$$
5	4	adantr	$$⊢\left(J\in V\wedge x\in X\right)\to \left\{y\in J|x\in y\right\}\in 𝒫J$$
6	5 1	fmptd	$$⊢J\in V\to F:X⟶𝒫J$$
7	6	ffnd	$$⊢J\in V\to FFnX$$