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

Metamath Proof Explorer

Theorem funimass1

Description: A kind of contraposition law that infers a subclass of an image from a preimage subclass. (Contributed by NM, 25-May-2004)

Ref Expression
Assertion funimass1 
|- ( ( Fun F /\ A C_ ran F ) -> ( ( `' F " A ) C_ B -> A C_ ( F " B ) ) )

Proof

Step Hyp Ref Expression
1 imass2 
 |-  ( ( `' F " A ) C_ B -> ( F " ( `' F " A ) ) C_ ( F " B ) )
2 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " A ) ) = ( A i^i ran F ) )
3 dfss 
 |-  ( A C_ ran F <-> A = ( A i^i ran F ) )
4 3 biimpi 
 |-  ( A C_ ran F -> A = ( A i^i ran F ) )
5 4 eqcomd 
 |-  ( A C_ ran F -> ( A i^i ran F ) = A )
6 2 5 sylan9eq 
 |-  ( ( Fun F /\ A C_ ran F ) -> ( F " ( `' F " A ) ) = A )
7 6 sseq1d 
 |-  ( ( Fun F /\ A C_ ran F ) -> ( ( F " ( `' F " A ) ) C_ ( F " B ) <-> A C_ ( F " B ) ) )
8 1 7 imbitrid 
 |-  ( ( Fun F /\ A C_ ran F ) -> ( ( `' F " A ) C_ B -> A C_ ( F " B ) ) )