This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnmpt2c

Description: A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmpt21.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt21.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
cnmpt2c.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
cnmpt2c.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑍 )
Assertion cnmpt2c ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑃 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnmpt21.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 cnmpt21.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3 cnmpt2c.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
4 cnmpt2c.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑍 )
5 eqidd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑃 = 𝑃 )
6 5 mpompt ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑃 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑃 )
7 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
9 8 3 4 cnmptc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑃 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )
10 6 9 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑃 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) )