Step | Hyp | Ref
| Expression |
1 | | df-dvn 25032 |
. . 3
⊢
D𝑛 = (𝑠
∈ 𝒫 ℂ, 𝑓
∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓}))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓})))) |
3 | | simprl 768 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → 𝑠 = 𝑆) |
4 | 3 | oveq1d 7290 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑠 D 𝑥) = (𝑆 D 𝑥)) |
5 | 4 | mpteq2dv 5176 |
. . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V ↦ (𝑠 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥))) |
6 | | dvnfval.1 |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) |
7 | 5, 6 | eqtr4di 2796 |
. . . . 5
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V ↦ (𝑠 D 𝑥)) = 𝐺) |
8 | 7 | coeq1d 5770 |
. . . 4
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ) = (𝐺 ∘ 1st
)) |
9 | 8 | seqeq2d 13728 |
. . 3
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝑓}))) |
10 | | simprr 770 |
. . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) |
11 | 10 | sneqd 4573 |
. . . . 5
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → {𝑓} = {𝐹}) |
12 | 11 | xpeq2d 5619 |
. . . 4
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 ×
{𝑓}) = (ℕ0
× {𝐹})) |
13 | 12 | seqeq3d 13729 |
. . 3
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝐹}))) |
14 | 9, 13 | eqtrd 2778 |
. 2
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝐹}))) |
15 | | simpr 485 |
. . 3
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
16 | 15 | oveq2d 7291 |
. 2
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑠 = 𝑆) → (ℂ ↑pm 𝑠) = (ℂ ↑pm
𝑆)) |
17 | | simpl 483 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝑆 ⊆
ℂ) |
18 | | cnex 10952 |
. . . 4
⊢ ℂ
∈ V |
19 | 18 | elpw2 5269 |
. . 3
⊢ (𝑆 ∈ 𝒫 ℂ ↔
𝑆 ⊆
ℂ) |
20 | 17, 19 | sylibr 233 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝑆 ∈ 𝒫
ℂ) |
21 | | simpr 485 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝐹 ∈ (ℂ
↑pm 𝑆)) |
22 | | seqex 13723 |
. . 3
⊢
seq0((𝐺 ∘
1st ), (ℕ0 × {𝐹})) ∈ V |
23 | 22 | a1i 11 |
. 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ seq0((𝐺 ∘
1st ), (ℕ0 × {𝐹})) ∈ V) |
24 | 2, 14, 16, 20, 21, 23 | ovmpodx 7424 |
1
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝑆
D𝑛 𝐹) =
seq0((𝐺 ∘
1st ), (ℕ0 × {𝐹}))) |