| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-dvn 25903 | . . 3
⊢ 
D𝑛 = (𝑠
∈ 𝒫 ℂ, 𝑓
∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓}))) | 
| 2 | 1 | a1i 11 | . 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓})))) | 
| 3 |  | simprl 771 | . . . . . . . 8
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → 𝑠 = 𝑆) | 
| 4 | 3 | oveq1d 7446 | . . . . . . 7
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑠 D 𝑥) = (𝑆 D 𝑥)) | 
| 5 | 4 | mpteq2dv 5244 | . . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V ↦ (𝑠 D 𝑥)) = (𝑥 ∈ V ↦ (𝑆 D 𝑥))) | 
| 6 |  | dvnfval.1 | . . . . . 6
⊢ 𝐺 = (𝑥 ∈ V ↦ (𝑆 D 𝑥)) | 
| 7 | 5, 6 | eqtr4di 2795 | . . . . 5
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ V ↦ (𝑠 D 𝑥)) = 𝐺) | 
| 8 | 7 | coeq1d 5872 | . . . 4
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ) = (𝐺 ∘ 1st
)) | 
| 9 | 8 | seqeq2d 14049 | . . 3
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝑓}))) | 
| 10 |  | simprr 773 | . . . . . 6
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) | 
| 11 | 10 | sneqd 4638 | . . . . 5
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → {𝑓} = {𝐹}) | 
| 12 | 11 | xpeq2d 5715 | . . . 4
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 ×
{𝑓}) = (ℕ0
× {𝐹})) | 
| 13 | 12 | seqeq3d 14050 | . . 3
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝐹}))) | 
| 14 | 9, 13 | eqtrd 2777 | . 2
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ),
(ℕ0 × {𝑓})) = seq0((𝐺 ∘ 1st ),
(ℕ0 × {𝐹}))) | 
| 15 |  | simpr 484 | . . 3
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) | 
| 16 | 15 | oveq2d 7447 | . 2
⊢ (((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
∧ 𝑠 = 𝑆) → (ℂ ↑pm 𝑠) = (ℂ ↑pm
𝑆)) | 
| 17 |  | simpl 482 | . . 3
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝑆 ⊆
ℂ) | 
| 18 |  | cnex 11236 | . . . 4
⊢ ℂ
∈ V | 
| 19 | 18 | elpw2 5334 | . . 3
⊢ (𝑆 ∈ 𝒫 ℂ ↔
𝑆 ⊆
ℂ) | 
| 20 | 17, 19 | sylibr 234 | . 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝑆 ∈ 𝒫
ℂ) | 
| 21 |  | simpr 484 | . 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ 𝐹 ∈ (ℂ
↑pm 𝑆)) | 
| 22 |  | seqex 14044 | . . 3
⊢
seq0((𝐺 ∘
1st ), (ℕ0 × {𝐹})) ∈ V | 
| 23 | 22 | a1i 11 | . 2
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ seq0((𝐺 ∘
1st ), (ℕ0 × {𝐹})) ∈ V) | 
| 24 | 2, 14, 16, 20, 21, 23 | ovmpodx 7584 | 1
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ (𝑆
D𝑛 𝐹) =
seq0((𝐺 ∘
1st ), (ℕ0 × {𝐹}))) |