Theorem fvimacnvALT

Description: Alternate proof of fvimacnv , based on funimass3 . If funimass3 is ever proved directly, as opposed to using funimacnv pointwise, then the proof of funimacnv should be replaced with this one. (Contributed by Raph Levien, 20-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fvimacnvALT	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )

Proof

Step	Hyp	Ref	Expression
1		snssi	|- ( A e. dom F -> { A } C_ dom F )
2		funimass3	|- ( ( Fun F /\ { A } C_ dom F ) -> ( ( F " { A } ) C_ B <-> { A } C_ ( `' F " B ) ) )
3	1 2	sylan2	|- ( ( Fun F /\ A e. dom F ) -> ( ( F " { A } ) C_ B <-> { A } C_ ( `' F " B ) ) )
4		fvex	|- ( F ` A ) e. _V
5	4	snss	|- ( ( F ` A ) e. B <-> { ( F ` A ) } C_ B )
6		eqid	|- dom F = dom F
7		df-fn	|- ( F Fn dom F <-> ( Fun F /\ dom F = dom F ) )
8	7	biimpri	|- ( ( Fun F /\ dom F = dom F ) -> F Fn dom F )
9	6 8	mpan2	|- ( Fun F -> F Fn dom F )
10		fnsnfv	|- ( ( F Fn dom F /\ A e. dom F ) -> { ( F ` A ) } = ( F " { A } ) )
11	9 10	sylan	|- ( ( Fun F /\ A e. dom F ) -> { ( F ` A ) } = ( F " { A } ) )
12	11	sseq1d	|- ( ( Fun F /\ A e. dom F ) -> ( { ( F ` A ) } C_ B <-> ( F " { A } ) C_ B ) )
13	5 12	bitrid	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> ( F " { A } ) C_ B ) )
14		snssg	|- ( A e. dom F -> ( A e. ( `' F " B ) <-> { A } C_ ( `' F " B ) ) )
15	14	adantl	|- ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " B ) <-> { A } C_ ( `' F " B ) ) )
16	3 13 15	3bitr4d	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )