Metamath Proof Explorer


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 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑓𝑀𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0fiubex ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ) )
2 ssel2 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑓𝑀 ) → 𝑓 ∈ ( 𝑅m0 ) )
3 2 ancoms ( ( 𝑓𝑀𝑀 ⊆ ( 𝑅m0 ) ) → 𝑓 ∈ ( 𝑅m0 ) )
4 elmapfn ( 𝑓 ∈ ( 𝑅m0 ) → 𝑓 Fn ℕ0 )
5 3 4 syl ( ( 𝑓𝑀𝑀 ⊆ ( 𝑅m0 ) ) → 𝑓 Fn ℕ0 )
6 5 expcom ( 𝑀 ⊆ ( 𝑅m0 ) → ( 𝑓𝑀𝑓 Fn ℕ0 ) )
7 6 3ad2ant1 ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( 𝑓𝑀𝑓 Fn ℕ0 ) )
8 7 adantr ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑓𝑀𝑓 Fn ℕ0 ) )
9 8 imp ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → 𝑓 Fn ℕ0 )
10 nn0ex 0 ∈ V
11 10 a1i ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → ℕ0 ∈ V )
12 simpll3 ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → 𝑍𝑉 )
13 suppvalfn ( ( 𝑓 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍𝑉 ) → ( 𝑓 supp 𝑍 ) = { 𝑥 ∈ ℕ0 ∣ ( 𝑓𝑥 ) ≠ 𝑍 } )
14 9 11 12 13 syl3anc ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → ( 𝑓 supp 𝑍 ) = { 𝑥 ∈ ℕ0 ∣ ( 𝑓𝑥 ) ≠ 𝑍 } )
15 14 sseq1d ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ { 𝑥 ∈ ℕ0 ∣ ( 𝑓𝑥 ) ≠ 𝑍 } ⊆ ( 0 ... 𝑚 ) ) )
16 rabss ( { 𝑥 ∈ ℕ0 ∣ ( 𝑓𝑥 ) ≠ 𝑍 } ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑓𝑥 ) ≠ 𝑍𝑥 ∈ ( 0 ... 𝑚 ) ) )
17 15 16 bitrdi ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑓𝑥 ) ≠ 𝑍𝑥 ∈ ( 0 ... 𝑚 ) ) ) )
18 nne ( ¬ ( 𝑓𝑥 ) ≠ 𝑍 ↔ ( 𝑓𝑥 ) = 𝑍 )
19 18 biimpi ( ¬ ( 𝑓𝑥 ) ≠ 𝑍 → ( 𝑓𝑥 ) = 𝑍 )
20 19 2a1d ( ¬ ( 𝑓𝑥 ) ≠ 𝑍 → ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ 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 syl6bi ( ( 𝑥 ∈ ℕ0𝑚 ∈ ℕ0 ) → ( 𝑥𝑚 → ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
28 27 3impia ( ( 𝑥 ∈ ℕ0𝑚 ∈ ℕ0𝑥𝑚 ) → ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) )
29 28 a1d ( ( 𝑥 ∈ ℕ0𝑚 ∈ ℕ0𝑥𝑚 ) → ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
30 21 29 sylbi ( 𝑥 ∈ ( 0 ... 𝑚 ) → ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
31 20 30 ja ( ( ( 𝑓𝑥 ) ≠ 𝑍𝑥 ∈ ( 0 ... 𝑚 ) ) → ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
32 31 com12 ( ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑓𝑥 ) ≠ 𝑍𝑥 ∈ ( 0 ... 𝑚 ) ) → ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
33 32 ralimdva ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → ( ∀ 𝑥 ∈ ℕ0 ( ( 𝑓𝑥 ) ≠ 𝑍𝑥 ∈ ( 0 ... 𝑚 ) ) → ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
34 17 33 sylbid ( ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓𝑀 ) → ( ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
35 34 ralimdva ( ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) ∧ 𝑚 ∈ ℕ0 ) → ( ∀ 𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) → ∀ 𝑓𝑀𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
36 35 reximdva ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∃ 𝑚 ∈ ℕ0𝑓𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑚 ) → ∃ 𝑚 ∈ ℕ0𝑓𝑀𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )
37 1 36 syld ( ( 𝑀 ⊆ ( 𝑅m0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍𝑉 ) → ( ∀ 𝑓𝑀 𝑓 finSupp 𝑍 → ∃ 𝑚 ∈ ℕ0𝑓𝑀𝑥 ∈ ℕ0 ( 𝑚 < 𝑥 → ( 𝑓𝑥 ) = 𝑍 ) ) )