Metamath Proof Explorer


Theorem fsuppmapnn0fz

Description: If a function over the nonnegative integers is finitely supported, then there is an upper bound for a finite set of sequential integers containing the support of the function. (Contributed by AV, 30-Sep-2019) (Proof shortened by AV, 6-Oct-2019)

Ref Expression
Assertion fsuppmapnn0fz ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) → ( 𝐹 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0ub ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) → ( 𝐹 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) ) )
2 simpllr ( ( ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) ) → 𝑍𝑉 )
3 simplll ( ( ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) ) → 𝐹 ∈ ( 𝑅m0 ) )
4 simplr ( ( ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) ) → 𝑚 ∈ ℕ0 )
5 simpr ( ( ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) )
6 2 3 4 5 suppssfz ( ( ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) ) → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) )
7 6 ex ( ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )
8 7 reximdva ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) → ( ∃ 𝑚 ∈ ℕ0𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹𝑥 ) = 𝑍 ) → ∃ 𝑚 ∈ ℕ0 ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )
9 1 8 syld ( ( 𝐹 ∈ ( 𝑅m0 ) ∧ 𝑍𝑉 ) → ( 𝐹 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )