Metamath Proof Explorer

Theorem imacosupp

Description: The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019)

Ref Expression
Assertion imacosupp 
|- ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) )

Proof

Step Hyp Ref Expression
1 suppco 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) )
2 1 imaeq2d 
 |-  ( ( F e. V /\ G e. W ) -> ( G " ( ( F o. G ) supp Z ) ) = ( G " ( `' G " ( F supp Z ) ) ) )
3 funforn 
 |-  ( Fun G <-> G : dom G -onto-> ran G )
4 foimacnv 
 |-  ( ( G : dom G -onto-> ran G /\ ( F supp Z ) C_ ran G ) -> ( G " ( `' G " ( F supp Z ) ) ) = ( F supp Z ) )
5 3 4 sylanb 
 |-  ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( `' G " ( F supp Z ) ) ) = ( F supp Z ) )
6 2 5 sylan9eq 
 |-  ( ( ( F e. V /\ G e. W ) /\ ( Fun G /\ ( F supp Z ) C_ ran G ) ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) )
7 6 ex 
 |-  ( ( F e. V /\ G e. W ) -> ( ( Fun G /\ ( F supp Z ) C_ ran G ) -> ( G " ( ( F o. G ) supp Z ) ) = ( F supp Z ) ) )