Theorem finnzfsuppd

Description: If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024)

	Ref	Expression
Hypotheses	finnzfsuppd.1	|- ( ph -> F e. V )
	finnzfsuppd.2	|- ( ph -> F Fn D )
	finnzfsuppd.3	|- ( ph -> Z e. U )
	finnzfsuppd.4	|- ( ph -> A e. Fin )
	finnzfsuppd.5	|- ( ( ph /\ x e. D ) -> ( x e. A \/ ( F ` x ) = Z ) )
Assertion	finnzfsuppd	|- ( ph -> F finSupp Z )

Proof

Step	Hyp	Ref	Expression
1		finnzfsuppd.1	|- ( ph -> F e. V )
2		finnzfsuppd.2	|- ( ph -> F Fn D )
3		finnzfsuppd.3	|- ( ph -> Z e. U )
4		finnzfsuppd.4	|- ( ph -> A e. Fin )
5		finnzfsuppd.5	|- ( ( ph /\ x e. D ) -> ( x e. A \/ ( F ` x ) = Z ) )
6	1 2	fndmexd	|- ( ph -> D e. _V )
7		elsuppfn	|- ( ( F Fn D /\ D e. _V /\ Z e. U ) -> ( x e. ( F supp Z ) <-> ( x e. D /\ ( F ` x ) =/= Z ) ) )
8	2 6 3 7	syl3anc	|- ( ph -> ( x e. ( F supp Z ) <-> ( x e. D /\ ( F ` x ) =/= Z ) ) )
9	8	biimpa	|- ( ( ph /\ x e. ( F supp Z ) ) -> ( x e. D /\ ( F ` x ) =/= Z ) )
10	9	simpld	|- ( ( ph /\ x e. ( F supp Z ) ) -> x e. D )
11	10 5	syldan	|- ( ( ph /\ x e. ( F supp Z ) ) -> ( x e. A \/ ( F ` x ) = Z ) )
12	9	simprd	|- ( ( ph /\ x e. ( F supp Z ) ) -> ( F ` x ) =/= Z )
13	12	neneqd	|- ( ( ph /\ x e. ( F supp Z ) ) -> -. ( F ` x ) = Z )
14	11 13	olcnd	|- ( ( ph /\ x e. ( F supp Z ) ) -> x e. A )
15	14	ex	|- ( ph -> ( x e. ( F supp Z ) -> x e. A ) )
16	15	ssrdv	|- ( ph -> ( F supp Z ) C_ A )
17	4 16	ssfid	|- ( ph -> ( F supp Z ) e. Fin )
18		fnfun	|- ( F Fn D -> Fun F )
19	2 18	syl	|- ( ph -> Fun F )
20		funisfsupp	|- ( ( Fun F /\ F e. V /\ Z e. U ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
21	19 1 3 20	syl3anc	|- ( ph -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
22	17 21	mpbird	|- ( ph -> F finSupp Z )