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

Metamath Proof Explorer

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 ) = (/) )