# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({F}:{A}⟶{B}\wedge {B}\subseteq {C}\right)\to {F}:{A}⟶{C}$

### Proof

Step Hyp Ref Expression
1 sstr2 ${⊢}\mathrm{ran}{F}\subseteq {B}\to \left({B}\subseteq {C}\to \mathrm{ran}{F}\subseteq {C}\right)$
2 1 com12 ${⊢}{B}\subseteq {C}\to \left(\mathrm{ran}{F}\subseteq {B}\to \mathrm{ran}{F}\subseteq {C}\right)$
3 2 anim2d ${⊢}{B}\subseteq {C}\to \left(\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)\to \left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {C}\right)\right)$
4 df-f ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)$
5 df-f ${⊢}{F}:{A}⟶{C}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {C}\right)$
6 3 4 5 3imtr4g ${⊢}{B}\subseteq {C}\to \left({F}:{A}⟶{B}\to {F}:{A}⟶{C}\right)$
7 6 impcom ${⊢}\left({F}:{A}⟶{B}\wedge {B}\subseteq {C}\right)\to {F}:{A}⟶{C}$