Theorem fdmfifsupp

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019)

	Ref	Expression
Hypotheses	fdmfisuppfi.f	|- ( ph -> F : D --> R )
	fdmfisuppfi.d	|- ( ph -> D e. Fin )
	fdmfisuppfi.z	|- ( ph -> Z e. V )
Assertion	fdmfifsupp	|- ( ph -> F finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		fdmfisuppfi.f	|- ( ph -> F : D --> R )
2		fdmfisuppfi.d	|- ( ph -> D e. Fin )
3		fdmfisuppfi.z	|- ( ph -> Z e. V )
4	1	ffund	|- ( ph -> Fun F )
5	1 2 3	fdmfisuppfi	|- ( ph -> ( F supp Z ) e. Fin )
6	1	ffnd	|- ( ph -> F Fn D )
7		fnex	|- ( ( F Fn D /\ D e. Fin ) -> F e. _V )
8	6 2 7	syl2anc	|- ( ph -> F e. _V )
9		isfsupp	|- ( ( F e. _V /\ Z e. V ) -> ( F finSupp Z <-> ( Fun F /\ ( F supp Z ) e. Fin ) ) )
10	8 3 9	syl2anc	|- ( ph -> ( F finSupp Z <-> ( Fun F /\ ( F supp Z ) e. Fin ) ) )
11	4 5 10	mpbir2and	|- ( ph -> F finSupp Z )