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	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) ∧ 𝐹 finSupp 𝑍 ) → 𝐹 finSupp 𝑍 )
2	1	fsuppimpd	⊢ ( ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) ∧ 𝐹 finSupp 𝑍 ) → ( 𝐹 supp 𝑍 ) ∈ Fin )
3	2	ex	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 → ( 𝐹 supp 𝑍 ) ∈ Fin ) )
4		elmapfn	⊢ ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) → 𝐹 Fn ℕ0 )
5	4	adantr	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → 𝐹 Fn ℕ0 )
6		nn0ex	⊢ ℕ0 ∈ V
7	6	a1i	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ℕ0 ∈ V )
8		simpr	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → 𝑍 ∈ 𝑉 )
9		suppvalfn	⊢ ( ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ ℕ0 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } )
10	5 7 8 9	syl3anc	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ ℕ0 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } )
11	10	eleq1d	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ↔ { 𝑥 ∈ ℕ0 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } ∈ Fin ) )
12		rabssnn0fi	⊢ ( { 𝑥 ∈ ℕ0 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } ∈ Fin ↔ ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
13		nne	⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
14	13	imbi2i	⊢ ( ( 𝑚 < 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ↔ ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
15	14	ralbii	⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
16	15	rexbii	⊢ ( ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ↔ ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
17	12 16	sylbb	⊢ ( { 𝑥 ∈ ℕ0 ∣ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 } ∈ Fin → ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
18	11 17	syl6bi	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin → ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) )
19	3 18	syld	⊢ ( ( 𝐹 ∈ ( 𝑅 ↑m ℕ0 ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝐹 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) )