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