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 )