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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion	kqffn	⊢ ( 𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2		ssrab2	⊢ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ⊆ 𝐽
3		elpw2g	⊢ ( 𝐽 ∈ 𝑉 → ( { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ∈ 𝒫 𝐽 ↔ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ⊆ 𝐽 ) )
4	2 3	mpbiri	⊢ ( 𝐽 ∈ 𝑉 → { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ∈ 𝒫 𝐽 )
5	4	adantr	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ∈ 𝒫 𝐽 )
6	5 1	fmptd	⊢ ( 𝐽 ∈ 𝑉 → 𝐹 : 𝑋 ⟶ 𝒫 𝐽 )
7	6	ffnd	⊢ ( 𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋 )