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

Metamath Proof Explorer

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