# Metamath Proof Explorer

## Theorem funimass2

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. (Contributed by NM, 25-May-2004)

Ref Expression
Assertion funimass2 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq {{F}}^{-1}\left[{B}\right]\right)\to {F}\left[{A}\right]\subseteq {B}$

### Proof

Step Hyp Ref Expression
1 funimacnv ${⊢}\mathrm{Fun}{F}\to {F}\left[{{F}}^{-1}\left[{B}\right]\right]={B}\cap \mathrm{ran}{F}$
2 1 sseq2d ${⊢}\mathrm{Fun}{F}\to \left({F}\left[{A}\right]\subseteq {F}\left[{{F}}^{-1}\left[{B}\right]\right]↔{F}\left[{A}\right]\subseteq {B}\cap \mathrm{ran}{F}\right)$
3 inss1 ${⊢}{B}\cap \mathrm{ran}{F}\subseteq {B}$
4 sstr2 ${⊢}{F}\left[{A}\right]\subseteq {B}\cap \mathrm{ran}{F}\to \left({B}\cap \mathrm{ran}{F}\subseteq {B}\to {F}\left[{A}\right]\subseteq {B}\right)$
5 3 4 mpi ${⊢}{F}\left[{A}\right]\subseteq {B}\cap \mathrm{ran}{F}\to {F}\left[{A}\right]\subseteq {B}$
6 2 5 syl6bi ${⊢}\mathrm{Fun}{F}\to \left({F}\left[{A}\right]\subseteq {F}\left[{{F}}^{-1}\left[{B}\right]\right]\to {F}\left[{A}\right]\subseteq {B}\right)$
7 imass2 ${⊢}{A}\subseteq {{F}}^{-1}\left[{B}\right]\to {F}\left[{A}\right]\subseteq {F}\left[{{F}}^{-1}\left[{B}\right]\right]$
8 6 7 impel ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq {{F}}^{-1}\left[{B}\right]\right)\to {F}\left[{A}\right]\subseteq {B}$