Theorem fsuppmapnn0fiub0

Description: If all functions of a finite set of functions over the nonnegative integers are finitely supported, then all these functions are zero for all integers greater than a fixed integer. (Contributed by AV, 3-Oct-2019)

	Ref	Expression
Assertion	fsuppmapnn0fiub0	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fsuppmapnn0fiubex	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )
2		ssel2	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → 𝑓 ∈ ( 𝑅 ↑m ℕ0 ) )
3	2	ancoms	⊢ ( ( 𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ) → 𝑓 ∈ ( 𝑅 ↑m ℕ0 ) )
4		elmapfn	⊢ ( 𝑓 ∈ ( 𝑅 ↑m ℕ0 ) → 𝑓 Fn ℕ0 )
5	3 4	syl	⊢ ( ( 𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ) → 𝑓 Fn ℕ0 )
6	5	expcom	⊢ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) → ( 𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0 ) )
7	6	3ad2ant1	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0 ) )
8	7	adantr	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0 ) )
9	8	imp	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → 𝑓 Fn ℕ0 )
10		nn0ex	⊢ ℕ0 ∈ V
11	10	a1i	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → ℕ0 ∈ V )
12		simpll3	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → 𝑍 ∈ 𝑉 )
13		suppvalfn	⊢ ( ( 𝑓 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 supp 𝑍 ) = { 𝑥 ∈ ℕ0 ∣ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 } )
14	9 11 12 13	syl3anc	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) = { 𝑥 ∈ ℕ0 ∣ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 } )
15	14	sseq1d	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ { 𝑥 ∈ ℕ0 ∣ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 } ⊆ ( 0 ... 𝑚 ) ) )
16		rabss	⊢ ( { 𝑥 ∈ ℕ0 ∣ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 } ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → 𝑥 ∈ ( 0 ... 𝑚 ) ) )
17	15 16	bitrdi	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → 𝑥 ∈ ( 0 ... 𝑚 ) ) ) )
18		nne	⊢ ( ¬ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 ↔ ( 𝑓 ‘ 𝑥 ) = 𝑍 )
19	18	biimpi	⊢ ( ¬ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → ( 𝑓 ‘ 𝑥 ) = 𝑍 )
20	19	2a1d	⊢ ( ¬ ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
21		elfz2nn0	⊢ ( 𝑥 ∈ ( 0 ... 𝑚 ) ↔ ( 𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑥 ≤ 𝑚 ) )
22		nn0re	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ )
23		nn0re	⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
24		lenlt	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( 𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥 ) )
25	22 23 24	syl2an	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥 ) )
26		pm2.21	⊢ ( ¬ 𝑚 < 𝑥 → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) )
27	25 26	biimtrdi	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑥 ≤ 𝑚 → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
28	27	3impia	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑥 ≤ 𝑚 ) → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) )
29	28	a1d	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑥 ≤ 𝑚 ) → ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
30	21 29	sylbi	⊢ ( 𝑥 ∈ ( 0 ... 𝑚 ) → ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
31	20 30	ja	⊢ ( ( ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → 𝑥 ∈ ( 0 ... 𝑚 ) ) → ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
32	31	com12	⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → 𝑥 ∈ ( 0 ... 𝑚 ) ) → ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
33	32	ralimdva	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → ( ∀ 𝑥 ∈ ℕ0 ( ( 𝑓 ‘ 𝑥 ) ≠ 𝑍 → 𝑥 ∈ ( 0 ... 𝑚 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
34	17 33	sylbid	⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
35	34	ralimdva	⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑚 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) → ∀ 𝑓 ∈ 𝑀 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
36	35	reximdva	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )
37	1 36	syld	⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0 ∀ 𝑓 ∈ 𝑀 ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓 ‘ 𝑥 ) = 𝑍 ) ) )