finnzfsuppd

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

Step	Hyp	Ref	Expression
1		finnzfsuppd.1	$⊢ φ \to F \in V$
2		finnzfsuppd.2	$⊢ φ \to F Fn D$
3		finnzfsuppd.3	$⊢ φ \to Z \in U$
4		finnzfsuppd.4	$⊢ φ \to A \in Fin$
5		finnzfsuppd.5	$⊢ (φ \land x \in D) \to (x \in A \lor F (x) = Z)$
6	1 2	fndmexd	$⊢ φ \to D \in V$
7		elsuppfn	$⊢ (F Fn D \land D \in V \land Z \in U) \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in D \land F (x) \neq Z))$
8	2 6 3 7	syl3anc	$⊢ φ \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in D \land F (x) \neq Z))$
9	8	biimpa	$⊢ (φ \land x \in {supp}_{Z} (F)) \to (x \in D \land F (x) \neq Z)$
10	9	simpld	$⊢ (φ \land x \in {supp}_{Z} (F)) \to x \in D$
11	10 5	syldan	$⊢ (φ \land x \in {supp}_{Z} (F)) \to (x \in A \lor F (x) = Z)$
12	9	simprd	$⊢ (φ \land x \in {supp}_{Z} (F)) \to F (x) \neq Z$
13	12	neneqd	$⊢ (φ \land x \in {supp}_{Z} (F)) \to \neg F (x) = Z$
14	11 13	olcnd	$⊢ (φ \land x \in {supp}_{Z} (F)) \to x \in A$
15	14	ex	$⊢ φ \to (x \in {supp}_{Z} (F) \to x \in A)$
16	15	ssrdv	$⊢ φ \to F supp Z \subseteq A$
17	4 16	ssfid	$⊢ φ \to F supp Z \in Fin$
18		fnfun	$⊢ F Fn D \to Fun F$
19	2 18	syl	$⊢ φ \to Fun F$
20		funisfsupp	$⊢ (Fun F \land F \in V \land Z \in U) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
21	19 1 3 20	syl3anc	$⊢ φ \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
22	17 21	mpbird	$⊢ φ \to {finSupp}_{Z} (F)$

Metamath Proof Explorer