Description: The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fdmfisuppfi.f | ||
fdmfisuppfi.d | |||
fdmfisuppfi.z | |||
Assertion | fdmfisuppfi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdmfisuppfi.f | ||
2 | fdmfisuppfi.d | ||
3 | fdmfisuppfi.z | ||
4 | 1 2 | fexd | |
5 | suppimacnv | ||
6 | 4 3 5 | syl2anc | |
7 | 2 1 | fisuppfi | |
8 | 6 7 | eqeltrd |