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

Metamath Proof Explorer

Theorem funimass2

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

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

Proof

Step Hyp Ref Expression
1 funimacnv 
 |-  ( Fun F -> ( F " ( `' F " B ) ) = ( B i^i ran F ) )
2 1 sseq2d 
 |-  ( Fun F -> ( ( F " A ) C_ ( F " ( `' F " B ) ) <-> ( F " A ) C_ ( B i^i ran F ) ) )
3 inss1 
 |-  ( B i^i ran F ) C_ B
4 sstr2 
 |-  ( ( F " A ) C_ ( B i^i ran F ) -> ( ( B i^i ran F ) C_ B -> ( F " A ) C_ B ) )
5 3 4 mpi 
 |-  ( ( F " A ) C_ ( B i^i ran F ) -> ( F " A ) C_ B )
6 2 5 biimtrdi 
 |-  ( Fun F -> ( ( F " A ) C_ ( F " ( `' F " B ) ) -> ( F " A ) C_ B ) )
7 imass2 
 |-  ( A C_ ( `' F " B ) -> ( F " A ) C_ ( F " ( `' F " B ) ) )
8 6 7 impel 
 |-  ( ( Fun F /\ A C_ ( `' F " B ) ) -> ( F " A ) C_ B )