Theorem suppssfz

Description: Condition for a function over the nonnegative integers to have a support contained in a finite set of sequential integers. (Contributed by AV, 9-Oct-2019)

	Ref	Expression
Hypotheses	suppssfz.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
	suppssfz.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
	suppssfz.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
	suppssfz.b	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
Assertion	suppssfz	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		suppssfz.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
2		suppssfz.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
3		suppssfz.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4		suppssfz.b	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
5		elmapfn	⊢ ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) → 𝐹 Fn ℕ0 )
6	2 5	syl	⊢ ( 𝜑 → 𝐹 Fn ℕ0 )
7		nn0ex	⊢ ℕ0 ∈ V
8	7	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
9	6 8 1	3jca	⊢ ( 𝜑 → ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) )
11		elsuppfn	⊢ ( ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) ) )
12	10 11	syl	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑛 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) ) )
13		breq2	⊢ ( 𝑥 = 𝑛 → ( 𝑆 < 𝑥 ↔ 𝑆 < 𝑛 ) )
14		fveqeq2	⊢ ( 𝑥 = 𝑛 → ( ( 𝐹 ‘ 𝑥 ) = 𝑍 ↔ ( 𝐹 ‘ 𝑛 ) = 𝑍 ) )
15	13 14	imbi12d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ↔ ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) ) )
16	15	rspcva	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) )
17		simplr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑛 ∈ ℕ0 )
18	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑆 ∈ ℕ0 )
19	18	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑆 ∈ ℕ0 )
20		nn0re	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
21		nn0re	⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ ℝ )
22	3 21	syl	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
23		lenlt	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 𝑛 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑛 ) )
24	20 22 23	syl2anr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑛 ) )
25	24	biimpar	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑛 ≤ 𝑆 )
26		elfz2nn0	⊢ ( 𝑛 ∈ ( 0 ... 𝑆 ) ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0 ∧ 𝑛 ≤ 𝑆 ) )
27	17 19 25 26	syl3anbrc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑛 ∈ ( 0 ... 𝑆 ) )
28	27	a1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
29	28	ex	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑆 < 𝑛 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
30		eqneqall	⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
31	30	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑛 ) = 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
32	29 31	jad	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
33	32	com23	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
34	33	ex	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
35	34	com14	⊢ ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
36	16 35	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
37	36	ex	⊢ ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) ) )
38	37	pm2.43a	⊢ ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
39	38	com23	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
40	39	imp	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
41	40	com13	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
42	41	imp	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
43	12 42	sylbid	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑛 ∈ ( 𝐹 supp 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
44	43	ssrdv	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )
45	4 44	mpdan	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )