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 ) ) )