Theorem fimacnvdisj

Description: The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007)

	Ref	Expression
Assertion	fimacnvdisj	|- ( ( F : A --> B /\ ( B i^i C ) = (/) ) -> ( `' F " C ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-rn	|- ran F = dom `' F
2		frn	|- ( F : A --> B -> ran F C_ B )
3	2	adantr	|- ( ( F : A --> B /\ ( B i^i C ) = (/) ) -> ran F C_ B )
4	1 3	eqsstrrid	|- ( ( F : A --> B /\ ( B i^i C ) = (/) ) -> dom `' F C_ B )
5		ssdisj	|- ( ( dom `' F C_ B /\ ( B i^i C ) = (/) ) -> ( dom `' F i^i C ) = (/) )
6	4 5	sylancom	|- ( ( F : A --> B /\ ( B i^i C ) = (/) ) -> ( dom `' F i^i C ) = (/) )
7		imadisj	|- ( ( `' F " C ) = (/) <-> ( dom `' F i^i C ) = (/) )
8	6 7	sylibr	|- ( ( F : A --> B /\ ( B i^i C ) = (/) ) -> ( `' F " C ) = (/) )