Proof of Theorem mptnn0fsuppr
Step | Hyp | Ref
| Expression |
1 | | mptnn0fsuppr.s |
. . 3
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐶) finSupp 0 ) |
2 | | fsuppimp 8164 |
. . . 4
⊢ ((𝑘 ∈ ℕ0
↦ 𝐶) finSupp 0 → (Fun
(𝑘 ∈
ℕ0 ↦ 𝐶) ∧ ((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) ∈
Fin)) |
3 | | mptnn0fsupp.c |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ 𝐵) |
4 | 3 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) |
5 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
↦ 𝐶) = (𝑘 ∈ ℕ0
↦ 𝐶) |
6 | 5 | fnmpt 5933 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵 → (𝑘 ∈ ℕ0
↦ 𝐶) Fn
ℕ0) |
7 | 4, 6 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ 𝐶) Fn
ℕ0) |
8 | | nn0ex 11175 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
9 | 8 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ0 ∈
V) |
10 | | mptnn0fsupp.0 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ 𝑉) |
11 | | elex 3185 |
. . . . . . . . . . . . . 14
⊢ ( 0 ∈ 𝑉 → 0 ∈ V) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ V) |
13 | 7, 9, 12 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ 𝐶) Fn ℕ0 ∧
ℕ0 ∈ V ∧ 0 ∈
V)) |
14 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → ((𝑘 ∈ ℕ0 ↦ 𝐶) Fn ℕ0 ∧
ℕ0 ∈ V ∧ 0 ∈
V)) |
15 | | suppvalfn 7189 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ0
↦ 𝐶) Fn
ℕ0 ∧ ℕ0 ∈ V ∧ 0 ∈ V) → ((𝑘 ∈ ℕ0
↦ 𝐶) supp 0 ) = {𝑥 ∈ ℕ0
∣ ((𝑘 ∈
ℕ0 ↦ 𝐶)‘𝑥) ≠ 0 }) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → ((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) = {𝑥 ∈ ℕ0 ∣ ((𝑘 ∈ ℕ0
↦ 𝐶)‘𝑥) ≠ 0 }) |
17 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) ∧ 𝑥 ∈ ℕ0) → 𝑥 ∈
ℕ0) |
18 | 4 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → ∀𝑘 ∈ ℕ0
𝐶 ∈ 𝐵) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) ∧ 𝑥 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) |
20 | | rspcsbela 3958 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 𝐶
∈ 𝐵) →
⦋𝑥 / 𝑘⦌𝐶 ∈ 𝐵) |
21 | 17, 19, 20 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) ∧ 𝑥 ∈ ℕ0) →
⦋𝑥 / 𝑘⦌𝐶 ∈ 𝐵) |
22 | 5 | fvmpts 6194 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℕ0
∧ ⦋𝑥 /
𝑘⦌𝐶 ∈ 𝐵) → ((𝑘 ∈ ℕ0 ↦ 𝐶)‘𝑥) = ⦋𝑥 / 𝑘⦌𝐶) |
23 | 17, 21, 22 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) ∧ 𝑥 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ 𝐶)‘𝑥) = ⦋𝑥 / 𝑘⦌𝐶) |
24 | 23 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) ∧ 𝑥 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ 𝐶)‘𝑥) ≠ 0 ↔
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 )) |
25 | 24 | rabbidva 3163 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → {𝑥 ∈ ℕ0 ∣ ((𝑘 ∈ ℕ0
↦ 𝐶)‘𝑥) ≠ 0 } = {𝑥 ∈ ℕ0 ∣
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 }) |
26 | 16, 25 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → ((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) = {𝑥 ∈ ℕ0 ∣
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 }) |
27 | 26 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → (((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) ∈ Fin ↔ {𝑥 ∈ ℕ0
∣ ⦋𝑥 /
𝑘⦌𝐶 ≠ 0 } ∈
Fin)) |
28 | 27 | biimpd 218 |
. . . . . . 7
⊢ ((𝜑 ∧ Fun (𝑘 ∈ ℕ0 ↦ 𝐶)) → (((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) ∈ Fin → {𝑥 ∈ ℕ0
∣ ⦋𝑥 /
𝑘⦌𝐶 ≠ 0 } ∈
Fin)) |
29 | 28 | expcom 450 |
. . . . . 6
⊢ (Fun
(𝑘 ∈
ℕ0 ↦ 𝐶) → (𝜑 → (((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) ∈ Fin → {𝑥 ∈ ℕ0
∣ ⦋𝑥 /
𝑘⦌𝐶 ≠ 0 } ∈
Fin))) |
30 | 29 | com23 84 |
. . . . 5
⊢ (Fun
(𝑘 ∈
ℕ0 ↦ 𝐶) → (((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) ∈ Fin → (𝜑 → {𝑥 ∈ ℕ0 ∣
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 } ∈
Fin))) |
31 | 30 | imp 444 |
. . . 4
⊢ ((Fun
(𝑘 ∈
ℕ0 ↦ 𝐶) ∧ ((𝑘 ∈ ℕ0 ↦ 𝐶) supp 0 ) ∈ Fin) →
(𝜑 → {𝑥 ∈ ℕ0 ∣
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 } ∈
Fin)) |
32 | 2, 31 | syl 17 |
. . 3
⊢ ((𝑘 ∈ ℕ0
↦ 𝐶) finSupp 0 → (𝜑 → {𝑥 ∈ ℕ0 ∣
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 } ∈
Fin)) |
33 | 1, 32 | mpcom 37 |
. 2
⊢ (𝜑 → {𝑥 ∈ ℕ0 ∣
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 } ∈
Fin) |
34 | | rabssnn0fi 12647 |
. . 3
⊢ ({𝑥 ∈ ℕ0
∣ ⦋𝑥 /
𝑘⦌𝐶 ≠ 0 } ∈ Fin ↔
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ¬ ⦋𝑥 / 𝑘⦌𝐶 ≠ 0 )) |
35 | | nne 2786 |
. . . . . 6
⊢ (¬
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 ↔
⦋𝑥 / 𝑘⦌𝐶 = 0 ) |
36 | 35 | imbi2i 325 |
. . . . 5
⊢ ((𝑠 < 𝑥 → ¬ ⦋𝑥 / 𝑘⦌𝐶 ≠ 0 ) ↔ (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐶 = 0 )) |
37 | 36 | ralbii 2963 |
. . . 4
⊢
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → ¬
⦋𝑥 / 𝑘⦌𝐶 ≠ 0 ) ↔ ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐶 = 0 )) |
38 | 37 | rexbii 3023 |
. . 3
⊢
(∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ¬ ⦋𝑥 / 𝑘⦌𝐶 ≠ 0 ) ↔ ∃𝑠 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 →
⦋𝑥 / 𝑘⦌𝐶 = 0 )) |
39 | 34, 38 | bitri 263 |
. 2
⊢ ({𝑥 ∈ ℕ0
∣ ⦋𝑥 /
𝑘⦌𝐶 ≠ 0 } ∈ Fin ↔
∃𝑠 ∈
ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐶 = 0 )) |
40 | 33, 39 | sylib 207 |
1
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → ⦋𝑥 / 𝑘⦌𝐶 = 0 )) |