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