Theorem mptnn0fsupp

Description: A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 5-Oct-2019) (Revised by AV, 23-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mptnn0fsupp.0	⊢ ( 𝜑 → 0 ∈ 𝑉 )
2		mptnn0fsupp.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
3		mptnn0fsupp.s	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
4	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
5		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) = ( 𝑘 ∈ ℕ0 ↦ 𝐶 )
6	5	fnmpt	⊢ ( ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
7	4 6	syl	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 )
8		nn0ex	⊢ ℕ0 ∈ V
9	8	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
10	1	elexd	⊢ ( 𝜑 → 0 ∈ V )
11		suppvalfn	⊢ ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) Fn ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
12	7 9 10 11	syl3anc	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) = { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } )
13		nne	⊢ ( ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 )
14		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
15	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 )
16		rspcsbela	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ∀ 𝑘 ∈ ℕ0 𝐶 ∈ 𝐵 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
17	14 15 16	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 )
18	5	fvmpts	⊢ ( ( 𝑥 ∈ ℕ0 ∧ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
19	14 17 18	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
20	19	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) = 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
21	13 20	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
22	21	imbi2d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) ↔ ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) )
23	22	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) )
24	23	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) ) )
25	3 24	mpbird	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) )
26		rabssnn0fi	⊢ ( { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 ) )
27	25 26	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ ℕ0 ∣ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 0 } ∈ Fin )
28	12 27	eqeltrd	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin )
29		funmpt	⊢ Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 )
30	8	mptex	⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ V
31		funisfsupp	⊢ ( ( Fun ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∧ ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) )
32	29 30 10 31	mp3an12i	⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 ↔ ( ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) supp 0 ) ∈ Fin ) )
33	28 32	mpbird	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )