Metamath Proof Explorer

Theorem supp0cosupp0

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

Ref Expression
Assertion supp0cosupp0 
|- ( ( F e. V /\ G e. W ) -> ( ( F supp Z ) = (/) -> ( ( F o. G ) 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 imaeq2 
 |-  ( ( F supp Z ) = (/) -> ( `' G " ( F supp Z ) ) = ( `' G " (/) ) )
3 ima0 
 |-  ( `' G " (/) ) = (/)
4 2 3 eqtrdi 
 |-  ( ( F supp Z ) = (/) -> ( `' G " ( F supp Z ) ) = (/) )
5 1 4 sylan9eq 
 |-  ( ( ( F e. V /\ G e. W ) /\ ( F supp Z ) = (/) ) -> ( ( F o. G ) supp Z ) = (/) )
6 5 ex 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F supp Z ) = (/) -> ( ( F o. G ) supp Z ) = (/) ) )