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 ) |