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

Metamath Proof Explorer

Theorem fnimaeq0

Description: Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 . (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Assertion fnimaeq0 
|- ( ( F Fn A /\ B C_ A ) -> ( ( F " B ) = (/) <-> B = (/) ) )

Proof

Step Hyp Ref Expression
1 imadisj 
 |-  ( ( F " B ) = (/) <-> ( dom F i^i B ) = (/) )
2 incom 
 |-  ( dom F i^i B ) = ( B i^i dom F )
3 fndm 
 |-  ( F Fn A -> dom F = A )
4 3 sseq2d 
 |-  ( F Fn A -> ( B C_ dom F <-> B C_ A ) )
5 4 biimpar 
 |-  ( ( F Fn A /\ B C_ A ) -> B C_ dom F )
6 dfss2 
 |-  ( B C_ dom F <-> ( B i^i dom F ) = B )
7 5 6 sylib 
 |-  ( ( F Fn A /\ B C_ A ) -> ( B i^i dom F ) = B )
8 2 7 eqtrid 
 |-  ( ( F Fn A /\ B C_ A ) -> ( dom F i^i B ) = B )
9 8 eqeq1d 
 |-  ( ( F Fn A /\ B C_ A ) -> ( ( dom F i^i B ) = (/) <-> B = (/) ) )
10 1 9 bitrid 
 |-  ( ( F Fn A /\ B C_ A ) -> ( ( F " B ) = (/) <-> B = (/) ) )