Metamath Proof Explorer


Theorem suppco

Description: The support of the composition of two functions is the inverse image by the inner function of the support of the outer function. (Contributed by AV, 30-May-2019) Extract this statement from the proof of supp0cosupp0 . (Revised by SN, 15-Sep-2023)

Ref Expression
Assertion suppco FVGWFGsuppZ=G-1FsuppZ

Proof

Step Hyp Ref Expression
1 coexg FVGWFGV
2 simpl ZVFVGWZV
3 suppimacnv FGVZVFGsuppZ=FG-1VZ
4 1 2 3 syl2an2 ZVFVGWFGsuppZ=FG-1VZ
5 cnvco FG-1=G-1F-1
6 5 imaeq1i FG-1VZ=G-1F-1VZ
7 6 a1i ZVFVGWFG-1VZ=G-1F-1VZ
8 imaco G-1F-1VZ=G-1F-1VZ
9 simprl ZVFVGWFV
10 suppimacnv FVZVFsuppZ=F-1VZ
11 9 2 10 syl2anc ZVFVGWFsuppZ=F-1VZ
12 11 imaeq2d ZVFVGWG-1FsuppZ=G-1F-1VZ
13 8 12 eqtr4id ZVFVGWG-1F-1VZ=G-1FsuppZ
14 4 7 13 3eqtrd ZVFVGWFGsuppZ=G-1FsuppZ
15 14 ex ZVFVGWFGsuppZ=G-1FsuppZ
16 prcnel ¬ZV¬ZV
17 16 intnand ¬ZV¬FGVZV
18 supp0prc ¬FGVZVFGsuppZ=
19 17 18 syl ¬ZVFGsuppZ=
20 16 intnand ¬ZV¬FVZV
21 supp0prc ¬FVZVFsuppZ=
22 20 21 syl ¬ZVFsuppZ=
23 22 imaeq2d ¬ZVG-1FsuppZ=G-1
24 ima0 G-1=
25 23 24 eqtrdi ¬ZVG-1FsuppZ=
26 19 25 eqtr4d ¬ZVFGsuppZ=G-1FsuppZ
27 26 a1d ¬ZVFVGWFGsuppZ=G-1FsuppZ
28 15 27 pm2.61i FVGWFGsuppZ=G-1FsuppZ