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

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 ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 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 𝑍 ) ) )