Metamath Proof Explorer


Theorem cncfss

Description: The set of continuous functions is expanded when the range 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 cncffvrn ( ( 𝐶 ⊆ ℂ ∧ 𝑓 ∈ ( 𝐴cn𝐵 ) ) → ( 𝑓 ∈ ( 𝐴cn𝐶 ) ↔ 𝑓 : 𝐴𝐶 ) )
6 5 adantll ( ( ( 𝐵𝐶𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴cn𝐵 ) ) → ( 𝑓 ∈ ( 𝐴cn𝐶 ) ↔ 𝑓 : 𝐴𝐶 ) )
7 4 6 mpbird ( ( ( 𝐵𝐶𝐶 ⊆ ℂ ) ∧ 𝑓 ∈ ( 𝐴cn𝐵 ) ) → 𝑓 ∈ ( 𝐴cn𝐶 ) )
8 7 ex ( ( 𝐵𝐶𝐶 ⊆ ℂ ) → ( 𝑓 ∈ ( 𝐴cn𝐵 ) → 𝑓 ∈ ( 𝐴cn𝐶 ) ) )
9 8 ssrdv ( ( 𝐵𝐶𝐶 ⊆ ℂ ) → ( 𝐴cn𝐵 ) ⊆ ( 𝐴cn𝐶 ) )