Description: The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fndmfisuppfi.f | |- ( ph -> F Fn D ) |
|
fndmfisuppfi.d | |- ( ph -> D e. Fin ) |
||
fndmfisuppfi.z | |- ( ph -> Z e. V ) |
||
Assertion | fndmfisuppfi | |- ( ph -> ( F supp Z ) e. Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fndmfisuppfi.f | |- ( ph -> F Fn D ) |
|
2 | fndmfisuppfi.d | |- ( ph -> D e. Fin ) |
|
3 | fndmfisuppfi.z | |- ( ph -> Z e. V ) |
|
4 | dffn3 | |- ( F Fn D <-> F : D --> ran F ) |
|
5 | 1 4 | sylib | |- ( ph -> F : D --> ran F ) |
6 | 5 2 3 | fdmfisuppfi | |- ( ph -> ( F supp Z ) e. Fin ) |