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	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		suppco	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) )
2	1	imaeq2d	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐺 “ ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) ) )
3		funforn	⊢ ( Fun 𝐺 ↔ 𝐺 : dom 𝐺 –onto→ ran 𝐺 )
4		foimacnv	⊢ ( ( 𝐺 : dom 𝐺 –onto→ ran 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 supp 𝑍 ) )
5	3 4	sylanb	⊢ ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) ) = ( 𝐹 supp 𝑍 ) )
6	2 5	sylan9eq	⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) )
7	6	ex	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) ) )