# Metamath Proof Explorer

## Theorem funimass3

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006)

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

### Proof

Step Hyp Ref Expression
1 funimass4 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({F}\left[{A}\right]\subseteq {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
2 ssel ${⊢}{A}\subseteq \mathrm{dom}{F}\to \left({x}\in {A}\to {x}\in \mathrm{dom}{F}\right)$
3 fvimacnv ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to \left({F}\left({x}\right)\in {B}↔{x}\in {{F}}^{-1}\left[{B}\right]\right)$
4 3 ex ${⊢}\mathrm{Fun}{F}\to \left({x}\in \mathrm{dom}{F}\to \left({F}\left({x}\right)\in {B}↔{x}\in {{F}}^{-1}\left[{B}\right]\right)\right)$
5 2 4 syl9r ${⊢}\mathrm{Fun}{F}\to \left({A}\subseteq \mathrm{dom}{F}\to \left({x}\in {A}\to \left({F}\left({x}\right)\in {B}↔{x}\in {{F}}^{-1}\left[{B}\right]\right)\right)\right)$
6 5 imp31 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)\in {B}↔{x}\in {{F}}^{-1}\left[{B}\right]\right)$
7 6 ralbidva ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {{F}}^{-1}\left[{B}\right]\right)$
8 1 7 bitrd ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({F}\left[{A}\right]\subseteq {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {{F}}^{-1}\left[{B}\right]\right)$
9 dfss3 ${⊢}{A}\subseteq {{F}}^{-1}\left[{B}\right]↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {{F}}^{-1}\left[{B}\right]$
10 8 9 syl6bbr ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({F}\left[{A}\right]\subseteq {B}↔{A}\subseteq {{F}}^{-1}\left[{B}\right]\right)$