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	$⊢ (B \subseteq C \land C \subseteq ℂ) \to A \underset{cn}{⟶} B \subseteq A \underset{cn}{⟶} C$

Step	Hyp	Ref	Expression
1		cncff	$⊢ f : A \underset{cn}{⟶} B \to f : A ⟶ B$
2	1	adantl	$⊢ ((B \subseteq C \land C \subseteq ℂ) \land f : A \underset{cn}{⟶} B) \to f : A ⟶ B$
3		simpll	$⊢ ((B \subseteq C \land C \subseteq ℂ) \land f : A \underset{cn}{⟶} B) \to B \subseteq C$
4	2 3	fssd	$⊢ ((B \subseteq C \land C \subseteq ℂ) \land f : A \underset{cn}{⟶} B) \to f : A ⟶ C$
5		cncfcdm	$⊢ (C \subseteq ℂ \land f : A \underset{cn}{⟶} B) \to (f : A \underset{cn}{⟶} C \leftrightarrow f : A ⟶ C)$
6	5	adantll	$⊢ ((B \subseteq C \land C \subseteq ℂ) \land f : A \underset{cn}{⟶} B) \to (f : A \underset{cn}{⟶} C \leftrightarrow f : A ⟶ C)$
7	4 6	mpbird	$⊢ ((B \subseteq C \land C \subseteq ℂ) \land f : A \underset{cn}{⟶} B) \to f : A \underset{cn}{⟶} C$
8	7	ex	$⊢ (B \subseteq C \land C \subseteq ℂ) \to (f : A \underset{cn}{⟶} B \to f : A \underset{cn}{⟶} C)$
9	8	ssrdv	$⊢ (B \subseteq C \land C \subseteq ℂ) \to A \underset{cn}{⟶} B \subseteq A \underset{cn}{⟶} C$

Metamath Proof Explorer