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

Metamath Proof Explorer

Theorem cncfss

Description: The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion cncfss ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) ⊆ ( 𝐴 –cn→ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cncff ⊢ ( 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
2 1 adantl ⊢ ( ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝑓 : 𝐴 ⟶ 𝐵 )
3 simpll ⊢ ( ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐵 ⊆ 𝐶 )
4 2 3 fssd ⊢ ( ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝑓 : 𝐴 ⟶ 𝐶 )
5 cncfcdm ⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝑓 ∈ ( 𝐴 –cn→ 𝐶 ) ↔ 𝑓 : 𝐴 ⟶ 𝐶 ) )
6 5 adantll ⊢ ( ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝑓 ∈ ( 𝐴 –cn→ 𝐶 ) ↔ 𝑓 : 𝐴 ⟶ 𝐶 ) )
7 4 6 mpbird ⊢ ( ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝑓 ∈ ( 𝐴 –cn→ 𝐶 ) )
8 7 ex ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) → ( 𝑓 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝑓 ∈ ( 𝐴 –cn→ 𝐶 ) ) )
9 8 ssrdv ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) ⊆ ( 𝐴 –cn→ 𝐶 ) )