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→ 𝐶 ) )