Metamath Proof Explorer


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 𝑋 )