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

Metamath Proof Explorer

Theorem addccncf2

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

Ref Expression
Hypothesis addccncf2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝑥 ) )
Assertion addccncf2 ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 addccncf2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝑥 ) )
2 simpl ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ⊆ ℂ )
3 simpr ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
4 ssidd ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ℂ ⊆ ℂ )
5 2 3 4 constcncfg ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
6 ssid ⊢ ℂ ⊆ ℂ
7 cncfmptid ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
8 6 7 mpan2 ⊢ ( 𝐴 ⊆ ℂ → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
9 8 adantr ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) ∈ ( 𝐴 –cn→ ℂ ) )
10 5 9 addcncf ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝑥 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
11 1 10 eqeltrid ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )