# Metamath Proof Explorer

## Theorem fvimacnv

Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006)

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

### Proof

Step Hyp Ref Expression
1 funfvop ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to ⟨{A},{F}\left({A}\right)⟩\in {F}$
2 fvex ${⊢}{F}\left({A}\right)\in \mathrm{V}$
3 opelcnvg ${⊢}\left({F}\left({A}\right)\in \mathrm{V}\wedge {A}\in \mathrm{dom}{F}\right)\to \left(⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}↔⟨{A},{F}\left({A}\right)⟩\in {F}\right)$
4 2 3 mpan ${⊢}{A}\in \mathrm{dom}{F}\to \left(⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}↔⟨{A},{F}\left({A}\right)⟩\in {F}\right)$
5 4 adantl ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left(⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}↔⟨{A},{F}\left({A}\right)⟩\in {F}\right)$
6 1 5 mpbird ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to ⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}$
7 elimasng ${⊢}\left({F}\left({A}\right)\in \mathrm{V}\wedge {A}\in \mathrm{dom}{F}\right)\to \left({A}\in {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]↔⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}\right)$
8 2 7 mpan ${⊢}{A}\in \mathrm{dom}{F}\to \left({A}\in {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]↔⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}\right)$
9 8 adantl ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left({A}\in {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]↔⟨{F}\left({A}\right),{A}⟩\in {{F}}^{-1}\right)$
10 6 9 mpbird ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to {A}\in {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]$
11 2 snss ${⊢}{F}\left({A}\right)\in {B}↔\left\{{F}\left({A}\right)\right\}\subseteq {B}$
12 imass2 ${⊢}\left\{{F}\left({A}\right)\right\}\subseteq {B}\to {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]\subseteq {{F}}^{-1}\left[{B}\right]$
13 11 12 sylbi ${⊢}{F}\left({A}\right)\in {B}\to {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]\subseteq {{F}}^{-1}\left[{B}\right]$
14 13 sseld ${⊢}{F}\left({A}\right)\in {B}\to \left({A}\in {{F}}^{-1}\left[\left\{{F}\left({A}\right)\right\}\right]\to {A}\in {{F}}^{-1}\left[{B}\right]\right)$
15 10 14 syl5com ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left({F}\left({A}\right)\in {B}\to {A}\in {{F}}^{-1}\left[{B}\right]\right)$
16 fvimacnvi ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in {{F}}^{-1}\left[{B}\right]\right)\to {F}\left({A}\right)\in {B}$
17 16 ex ${⊢}\mathrm{Fun}{F}\to \left({A}\in {{F}}^{-1}\left[{B}\right]\to {F}\left({A}\right)\in {B}\right)$
18 17 adantr ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left({A}\in {{F}}^{-1}\left[{B}\right]\to {F}\left({A}\right)\in {B}\right)$
19 15 18 impbid ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to \left({F}\left({A}\right)\in {B}↔{A}\in {{F}}^{-1}\left[{B}\right]\right)$