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

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 ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )

Proof

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