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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
finnzfsuppd.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
finnzfsuppd.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
finnzfsuppd.4 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
finnzfsuppd.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
Assertion finnzfsuppd ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 finnzfsuppd.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 finnzfsuppd.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
3 finnzfsuppd.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
4 finnzfsuppd.4 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 finnzfsuppd.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
6 1 2 fndmexd ⊢ ( 𝜑 → 𝐷 ∈ V )
7 elsuppfn ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐷 ∈ V ∧ 𝑍 ∈ 𝑈 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ) )
8 2 6 3 7 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ) )
9 8 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → ( 𝑥 ∈ 𝐷 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
10 9 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → 𝑥 ∈ 𝐷 )
11 10 5 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → ( 𝑥 ∈ 𝐴 ∨ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
12 9 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 )
13 12 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → ¬ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
14 11 13 olcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) → 𝑥 ∈ 𝐴 )
15 14 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) → 𝑥 ∈ 𝐴 ) )
16 15 ssrdv ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝐴 )
17 4 16 ssfid ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
18 fnfun ⊢ ( 𝐹 Fn 𝐷 → Fun 𝐹 )
19 2 18 syl ⊢ ( 𝜑 → Fun 𝐹 )
20 funisfsupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈 ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
21 19 1 3 20 syl3anc ⊢ ( 𝜑 → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
22 17 21 mpbird ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )