Theorem mptnn0fsuppr

Description: A finitely supported mapping from the nonnegative integers fulfills certain conditions. (Contributed by AV, 3-Nov-2019) (Revised by AV, 23-Dec-2019)

	Ref	Expression
Hypotheses	mptnn0fsupp.0	⊢ ( 𝜑 → 0 ∈ 𝑉 )
	mptnn0fsupp.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
	mptnn0fsuppr.s	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )
Assertion	mptnn0fsuppr	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		mptnn0fsupp.0	⊢ ( 𝜑 → 0 ∈ 𝑉 )
2		mptnn0fsupp.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
3		mptnn0fsuppr.s	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )
4		fsuppimp	⊢ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 → ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) )
5	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
6		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐶 )
7	6	fnmpt	⊢ ( ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
8	5 7	syl	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
9		nn0ex	⊢ ℕ0 ∈ V
10	9	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
11	1	elexd	⊢ ( 𝜑 → 0 ∈ V )
12	8 10 11	3jca	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) )
14		suppvalfn	⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
15	13 14	syl	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
16		simpr	⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
17	5	adantr	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
18	17	adantr	⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
19		rspcsbela	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
20	16 18 19	syl2anc	⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
21	6	fvmpts	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
22	16 20 21	syl2anc	⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
23	22	neeq1d	⊢ ( ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) )
24	23	rabbidva	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } = { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } )
25	15 24	eqtrd	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } )
26	25	eleq1d	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ↔ { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
27	26	biimpd	⊢ ( ( 𝜑 ∧ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
28	27	expcom	⊢ ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) → ( 𝜑 → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) ) )
29	28	com23	⊢ ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin → ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) ) )
30	29	imp	⊢ ( ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∧ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) → ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
31	4 30	syl	⊢ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 → ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ) )
32	3 31	mpcom	⊢ ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin )
33		rabssnn0fi	⊢ ( { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) )
34		nne	⊢ ( ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 )
35	34	imbi2i	⊢ ( ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) ↔ ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
36	35	ralbii	⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
37	36	rexbii	⊢ ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
38	33 37	bitri	⊢ ( { 𝑥 ∈ ℕ0 ∣ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ≠ 0 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
39	32 38	sylib	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )