| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-limc 23630 |
. . . 4
⊢
limℂ = (𝑓
∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣
[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}) |
| 2 | 1 | a1i 11 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) →
limℂ = (𝑓
∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣
[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})) |
| 3 | | fvexd 6203 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
(TopOpen‘ℂfld) ∈ V) |
| 4 | | simplrl 800 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑓 = 𝐹) |
| 5 | 4 | dmeqd 5326 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = dom 𝐹) |
| 6 | | simpll1 1100 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝐹:𝐴⟶ℂ) |
| 7 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝐹 = 𝐴) |
| 9 | 5, 8 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = 𝐴) |
| 10 | | simplrr 801 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑥 = 𝐵) |
| 11 | 10 | sneqd 4189 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ {𝑥} = {𝐵}) |
| 12 | 9, 11 | uneq12d 3768 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (dom 𝑓 ∪ {𝑥}) = (𝐴 ∪ {𝐵})) |
| 13 | 10 | eqeq2d 2632 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 = 𝑥 ↔ 𝑧 = 𝐵)) |
| 14 | 4 | fveq1d 6193 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑓‘𝑧) = (𝐹‘𝑧)) |
| 15 | 13, 14 | ifbieq2d 4111 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧)) = if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 16 | 12, 15 | mpteq12dv 4733 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧)))) |
| 17 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 =
(TopOpen‘ℂfld)) |
| 18 | | limcval.k |
. . . . . . . . . . 11
⊢ 𝐾 =
(TopOpen‘ℂfld) |
| 19 | 17, 18 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 = 𝐾) |
| 20 | 19, 12 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
| 21 | | limcval.j |
. . . . . . . . 9
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
| 22 | 20, 21 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = 𝐽) |
| 23 | 22, 19 | oveq12d 6668 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗) = (𝐽 CnP 𝐾)) |
| 24 | 23, 10 | fveq12d 6197 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗)‘𝑥) = ((𝐽 CnP 𝐾)‘𝐵)) |
| 25 | 16, 24 | eleq12d 2695 |
. . . . 5
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑧 ∈ (dom
𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 26 | 3, 25 | sbcied 3472 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
([(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 27 | 26 | abbidv 2741 |
. . 3
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) → {𝑦 ∣
[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)} = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 28 | | cnex 10017 |
. . . . 5
⊢ ℂ
∈ V |
| 29 | | elpm2r 7875 |
. . . . 5
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 30 | 28, 28, 29 | mpanl12 718 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 31 | 30 | 3adant3 1081 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 32 | | simp3 1063 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
| 33 | | eqid 2622 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 34 | 21, 18, 33 | limcvallem 23635 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝑦 ∈ ℂ)) |
| 35 | 34 | abssdv 3676 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ) |
| 36 | 28 | ssex 4802 |
. . . 4
⊢ ({𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 37 | 35, 36 | syl 17 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 38 | 2, 27, 31, 32, 37 | ovmpt2d 6788 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 39 | 38, 35 | eqsstrd 3639 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) ⊆ ℂ) |
| 40 | 38, 39 | jca 554 |
1
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) |
