fss

Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	fss	$⊢ (F : A ⟶ B \land B \subseteq C) \to F : A ⟶ C$

Step	Hyp	Ref	Expression
1		sstr2	$⊢ ran F \subseteq B \to (B \subseteq C \to ran F \subseteq C)$
2	1	com12	$⊢ B \subseteq C \to (ran F \subseteq B \to ran F \subseteq C)$
3	2	anim2d	$⊢ B \subseteq C \to ((F Fn A \land ran F \subseteq B) \to (F Fn A \land ran F \subseteq C))$
4		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
5		df-f	$⊢ F : A ⟶ C \leftrightarrow (F Fn A \land ran F \subseteq C)$
6	3 4 5	3imtr4g	$⊢ B \subseteq C \to (F : A ⟶ B \to F : A ⟶ C)$
7	6	impcom	$⊢ (F : A ⟶ B \land B \subseteq C) \to F : A ⟶ C$

Metamath Proof Explorer