Metamath Proof Explorer

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 ⊢ φ → F ∈ V
finnzfsuppd.2 ⊢ φ → F Fn D
finnzfsuppd.3 ⊢ φ → Z ∈ U
finnzfsuppd.4 ⊢ φ → A ∈ Fin
finnzfsuppd.5 ⊢ φ ∧ x ∈ D → x ∈ A ∨ F ⁡ x = Z
Assertion finnzfsuppd ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 finnzfsuppd.1 ⊢ φ → F ∈ V
2 finnzfsuppd.2 ⊢ φ → F Fn D
3 finnzfsuppd.3 ⊢ φ → Z ∈ U
4 finnzfsuppd.4 ⊢ φ → A ∈ Fin
5 finnzfsuppd.5 ⊢ φ ∧ x ∈ D → x ∈ A ∨ F ⁡ x = Z
6 1 2 fndmexd ⊢ φ → D ∈ V
7 elsuppfn ⊢ F Fn D ∧ D ∈ V ∧ Z ∈ U → x ∈ supp Z⁡ F ↔ x ∈ D ∧ F ⁡ x ≠ Z
8 2 6 3 7 syl3anc ⊢ φ → x ∈ supp Z⁡ F ↔ x ∈ D ∧ F ⁡ x ≠ Z
9 8 biimpa ⊢ φ ∧ x ∈ supp Z⁡ F → x ∈ D ∧ F ⁡ x ≠ Z
10 9 simpld ⊢ φ ∧ x ∈ supp Z⁡ F → x ∈ D
11 10 5 syldan ⊢ φ ∧ x ∈ supp Z⁡ F → x ∈ A ∨ F ⁡ x = Z
12 9 simprd ⊢ φ ∧ x ∈ supp Z⁡ F → F ⁡ x ≠ Z
13 12 neneqd ⊢ φ ∧ x ∈ supp Z⁡ F → ¬ F ⁡ x = Z
14 11 13 olcnd ⊢ φ ∧ x ∈ supp Z⁡ F → x ∈ A
15 14 ex ⊢ φ → x ∈ supp Z⁡ F → x ∈ A
16 15 ssrdv ⊢ φ → F supp Z ⊆ A
17 4 16 ssfid ⊢ φ → F supp Z ∈ Fin
18 fnfun ⊢ F Fn D → Fun ⁡ F
19 2 18 syl ⊢ φ → Fun ⁡ F
20 funisfsupp ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ U → finSupp Z⁡ F ↔ F supp Z ∈ Fin
21 19 1 3 20 syl3anc ⊢ φ → finSupp Z⁡ F ↔ F supp Z ∈ Fin
22 17 21 mpbird ⊢ φ → finSupp Z⁡ F