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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coexg | |
|
2 | simpl | |
|
3 | suppimacnv | |
|
4 | 1 2 3 | syl2an2 | |
5 | cnvco | |
|
6 | 5 | imaeq1i | |
7 | 6 | a1i | |
8 | imaco | |
|
9 | simprl | |
|
10 | suppimacnv | |
|
11 | 9 2 10 | syl2anc | |
12 | 11 | imaeq2d | |
13 | 8 12 | eqtr4id | |
14 | 4 7 13 | 3eqtrd | |
15 | 14 | ex | |
16 | prcnel | |
|
17 | 16 | intnand | |
18 | supp0prc | |
|
19 | 17 18 | syl | |
20 | 16 | intnand | |
21 | supp0prc | |
|
22 | 20 21 | syl | |
23 | 22 | imaeq2d | |
24 | ima0 | |
|
25 | 23 24 | eqtrdi | |
26 | 19 25 | eqtr4d | |
27 | 26 | a1d | |
28 | 15 27 | pm2.61i | |