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 )