This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐷 = 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 )