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

Metamath Proof Explorer

Theorem constcncfg

Description: A constant function is a continuous function on CC . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses constcncfg.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
constcncfg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
constcncfg.c ⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
Assertion constcncfg ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 constcncfg.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2 constcncfg.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐶 )
3 constcncfg.c ⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
4 cncfmptc ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
5 2 1 3 4 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )