This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )

Proof

Step Hyp Ref Expression
1 funfvop 
 |-  ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
2 fvex 
 |-  ( F ` A ) e. _V
3 opelcnvg 
 |-  ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
4 2 3 mpan 
 |-  ( A e. dom F -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
5 4 adantl 
 |-  ( ( Fun F /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
6 1 5 mpbird 
 |-  ( ( Fun F /\ A e. dom F ) -> <. ( F ` A ) , A >. e. `' F )
7 elimasng 
 |-  ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
8 2 7 mpan 
 |-  ( A e. dom F -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
9 8 adantl 
 |-  ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
10 6 9 mpbird 
 |-  ( ( Fun F /\ A e. dom F ) -> A e. ( `' F " { ( F ` A ) } ) )
11 2 snss 
 |-  ( ( F ` A ) e. B <-> { ( F ` A ) } C_ B )
12 imass2 
 |-  ( { ( F ` A ) } C_ B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )
13 11 12 sylbi 
 |-  ( ( F ` A ) e. B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )
14 13 sseld 
 |-  ( ( F ` A ) e. B -> ( A e. ( `' F " { ( F ` A ) } ) -> A e. ( `' F " B ) ) )
15 10 14 syl5com 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) )
16 fvimacnvi 
 |-  ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )
17 16 ex 
 |-  ( Fun F -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
18 17 adantr 
 |-  ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
19 15 18 impbid 
 |-  ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )