Description: The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cnmptk1.j | ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) | |
| cnmptk1.k | ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) | ||
| Assertion | cnmptkc | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝑥 ) ) ∈ ( 𝐽 Cn ( 𝐽 ↑ko 𝐾 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnmptk1.j | ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) | |
| 2 | cnmptk1.k | ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) | |
| 3 | fconstmpt | ⊢ ( 𝑌 × { 𝑥 } ) = ( 𝑦 ∈ 𝑌 ↦ 𝑥 ) | |
| 4 | 3 | mpteq2i | ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑌 × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝑥 ) ) |
| 5 | xkoccn | ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑥 ∈ 𝑋 ↦ ( 𝑌 × { 𝑥 } ) ) ∈ ( 𝐽 Cn ( 𝐽 ↑ko 𝐾 ) ) ) | |
| 6 | 2 1 5 | syl2anc | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑌 × { 𝑥 } ) ) ∈ ( 𝐽 Cn ( 𝐽 ↑ko 𝐾 ) ) ) |
| 7 | 4 6 | eqeltrrid | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝑥 ) ) ∈ ( 𝐽 Cn ( 𝐽 ↑ko 𝐾 ) ) ) |