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 ( ( 𝐹𝑉𝐺𝑊 ) → ( ( 𝐹 supp 𝑍 ) = ∅ → ( ( 𝐹𝐺 ) supp 𝑍 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 suppco ( ( 𝐹𝑉𝐺𝑊 ) → ( ( 𝐹𝐺 ) supp 𝑍 ) = ( 𝐺 “ ( 𝐹 supp 𝑍 ) ) )
2 imaeq2 ( ( 𝐹 supp 𝑍 ) = ∅ → ( 𝐺 “ ( 𝐹 supp 𝑍 ) ) = ( 𝐺 “ ∅ ) )
3 ima0 ( 𝐺 “ ∅ ) = ∅
4 2 3 eqtrdi ( ( 𝐹 supp 𝑍 ) = ∅ → ( 𝐺 “ ( 𝐹 supp 𝑍 ) ) = ∅ )
5 1 4 sylan9eq ( ( ( 𝐹𝑉𝐺𝑊 ) ∧ ( 𝐹 supp 𝑍 ) = ∅ ) → ( ( 𝐹𝐺 ) supp 𝑍 ) = ∅ )
6 5 ex ( ( 𝐹𝑉𝐺𝑊 ) → ( ( 𝐹 supp 𝑍 ) = ∅ → ( ( 𝐹𝐺 ) supp 𝑍 ) = ∅ ) )