Metamath Proof Explorer

Theorem imacosuppOLD

Description: Obsolete version of imacosupp as of 15-Sep-2023. The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion imacosuppOLD ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 cnvco ⊢ ◡ ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 ∘ ◡ 𝐹 )
2 1 imaeq1i ⊢ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐺 ∘ ◡ 𝐹 ) “ ( V ∖ { 𝑍 } ) )
3 imaco ⊢ ( ( ◡ 𝐺 ∘ ◡ 𝐹 ) “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
4 2 3 eqtri ⊢ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
5 4 imaeq2i ⊢ ( 𝐺 “ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ) = ( 𝐺 “ ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
6 funforn ⊢ ( Fun 𝐺 ↔ 𝐺 : dom 𝐺 –onto→ ran 𝐺 )
7 6 biimpi ⊢ ( Fun 𝐺 → 𝐺 : dom 𝐺 –onto→ ran 𝐺 )
8 7 ad2antrl ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → 𝐺 : dom 𝐺 –onto→ ran 𝐺 )
9 simpl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐹 ∈ 𝑉 )
10 9 anim2i ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝑍 ∈ V ∧ 𝐹 ∈ 𝑉 ) )
11 10 ancomd ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ V ) )
12 suppimacnv ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
13 11 12 syl ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
14 13 sseq1d ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ↔ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ran 𝐺 ) )
15 14 biimpd ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ran 𝐺 ) )
16 15 adantld ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ran 𝐺 ) )
17 16 imp ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ran 𝐺 )
18 foimacnv ⊢ ( ( 𝐺 : dom 𝐺 –onto→ ran 𝐺 ∧ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
19 8 17 18 syl2anc ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
20 5 19 syl5eq ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( 𝐺 “ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
21 coexg ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
22 21 anim2i ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝑍 ∈ V ∧ ( 𝐹 ∘ 𝐺 ) ∈ V ) )
23 22 ancomd ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) )
24 suppimacnv ⊢ ( ( ( 𝐹 ∘ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
25 23 24 syl ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
26 25 imaeq2d ⊢ ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐺 “ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ) )
27 26 adantr ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐺 “ ( ◡ ( 𝐹 ∘ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ) )
28 13 adantr ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
29 20 27 28 3eqtr4d ⊢ ( ( ( 𝑍 ∈ V ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ) ∧ ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) )
30 29 exp31 ⊢ ( 𝑍 ∈ V → ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) ) ) )
31 ima0 ⊢ ( 𝐺 “ ∅ ) = ∅
32 id ⊢ ( ¬ 𝑍 ∈ V → ¬ 𝑍 ∈ V )
33 32 intnand ⊢ ( ¬ 𝑍 ∈ V → ¬ ( ( 𝐹 ∘ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) )
34 supp0prc ⊢ ( ¬ ( ( 𝐹 ∘ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ∅ )
35 33 34 syl ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ∅ )
36 35 imaeq2d ⊢ ( ¬ 𝑍 ∈ V → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐺 “ ∅ ) )
37 32 intnand ⊢ ( ¬ 𝑍 ∈ V → ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) )
38 supp0prc ⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ∅ )
39 37 38 syl ⊢ ( ¬ 𝑍 ∈ V → ( 𝐹 supp 𝑍 ) = ∅ )
40 31 36 39 3eqtr4a ⊢ ( ¬ 𝑍 ∈ V → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) )
41 40 2a1d ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) ) ) )
42 30 41 pm2.61i ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( Fun 𝐺 ∧ ( 𝐹 supp 𝑍 ) ⊆ ran 𝐺 ) → ( 𝐺 “ ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ) = ( 𝐹 supp 𝑍 ) ) )