This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsuppmapnn0ub

Description: If a function over the nonnegative integers is finitely supported, then there is an upper bound for the arguments resulting in nonzero values. (Contributed by AV, 6-Oct-2019)

Ref Expression
Assertion fsuppmapnn0ub ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → finSupp Z⁡ F → ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → F ⁡ x = Z

Proof

Step Hyp Ref Expression
1 simpr ⊢ F ∈ R ℕ 0 ∧ Z ∈ V ∧ finSupp Z⁡ F → finSupp Z⁡ F
2 1 fsuppimpd ⊢ F ∈ R ℕ 0 ∧ Z ∈ V ∧ finSupp Z⁡ F → F supp Z ∈ Fin
3 2 ex ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → finSupp Z⁡ F → F supp Z ∈ Fin
4 elmapfn ⊢ F ∈ R ℕ 0 → F Fn ℕ 0
5 4 adantr ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → F Fn ℕ 0
6 nn0ex ⊢ ℕ 0 ∈ V
7 6 a1i ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → ℕ 0 ∈ V
8 simpr ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → Z ∈ V
9 suppvalfn ⊢ F Fn ℕ 0 ∧ ℕ 0 ∈ V ∧ Z ∈ V → F supp Z = x ∈ ℕ 0 | F ⁡ x ≠ Z
10 5 7 8 9 syl3anc ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → F supp Z = x ∈ ℕ 0 | F ⁡ x ≠ Z
11 10 eleq1d ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → F supp Z ∈ Fin ↔ x ∈ ℕ 0 | F ⁡ x ≠ Z ∈ Fin
12 rabssnn0fi ⊢ x ∈ ℕ 0 | F ⁡ x ≠ Z ∈ Fin ↔ ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → ¬ F ⁡ x ≠ Z
13 nne ⊢ ¬ F ⁡ x ≠ Z ↔ F ⁡ x = Z
14 13 imbi2i ⊢ m < x → ¬ F ⁡ x ≠ Z ↔ m < x → F ⁡ x = Z
15 14 ralbii ⊢ ∀ x ∈ ℕ 0 m < x → ¬ F ⁡ x ≠ Z ↔ ∀ x ∈ ℕ 0 m < x → F ⁡ x = Z
16 15 rexbii ⊢ ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → ¬ F ⁡ x ≠ Z ↔ ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → F ⁡ x = Z
17 12 16 sylbb ⊢ x ∈ ℕ 0 | F ⁡ x ≠ Z ∈ Fin → ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → F ⁡ x = Z
18 11 17 biimtrdi ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → F supp Z ∈ Fin → ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → F ⁡ x = Z
19 3 18 syld ⊢ F ∈ R ℕ 0 ∧ Z ∈ V → finSupp Z⁡ F → ∃ m ∈ ℕ 0 ∀ x ∈ ℕ 0 m < x → F ⁡ x = Z