Metamath Proof Explorer


Theorem fndmfisuppfi

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 )

Proof

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 )