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