Theorem mptnn0fsuppd

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

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

Proof

Step	Hyp	Ref	Expression
1		mptnn0fsupp.0	⊢ ( 𝜑 → 0 ∈ 𝑉 )
2		mptnn0fsupp.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ 𝐵 )
3		mptnn0fsuppd.d	⊢ ( 𝑘 = 𝑥 → 𝐶 = 𝐷 )
4		mptnn0fsuppd.s	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → 𝐷 = 0 ) )
5		vex	⊢ 𝑥 ∈ V
6	5 3	csbie	⊢ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 𝐷
7		id	⊢ ( 𝐷 = 0 → 𝐷 = 0 )
8	6 7	syl5eq	⊢ ( 𝐷 = 0 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 )
9	8	imim2i	⊢ ( ( 𝑠 < 𝑥 → 𝐷 = 0 ) → ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
10	9	ralimi	⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → 𝐷 = 0 ) → ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
11	10	reximi	⊢ ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → 𝐷 = 0 ) → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
12	4 11	syl	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 = 0 ) )
13	1 2 12	mptnn0fsupp	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐶 ) finSupp 0 )