| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-limc 25230 |
. . . 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 6857 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
(TopOpen‘ℂfld) ∈ V) |
| 4 | | simplrl 775 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑓 = 𝐹) |
| 5 | 4 | dmeqd 5861 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = dom 𝐹) |
| 6 | | simpll1 1212 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝐹:𝐴⟶ℂ) |
| 7 | 6 | fdmd 6679 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝐹 = 𝐴) |
| 8 | 5, 7 | eqtrd 2776 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = 𝐴) |
| 9 | | simplrr 776 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑥 = 𝐵) |
| 10 | 9 | sneqd 4598 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ {𝑥} = {𝐵}) |
| 11 | 8, 10 | uneq12d 4124 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (dom 𝑓 ∪ {𝑥}) = (𝐴 ∪ {𝐵})) |
| 12 | 9 | eqeq2d 2747 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 = 𝑥 ↔ 𝑧 = 𝐵)) |
| 13 | 4 | fveq1d 6844 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑓‘𝑧) = (𝐹‘𝑧)) |
| 14 | 12, 13 | ifbieq2d 4512 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧)) = if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 15 | 11, 14 | mpteq12dv 5196 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧)))) |
| 16 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 =
(TopOpen‘ℂfld)) |
| 17 | | limcval.k |
. . . . . . . . . . 11
⊢ 𝐾 =
(TopOpen‘ℂfld) |
| 18 | 16, 17 | eqtr4di 2794 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 = 𝐾) |
| 19 | 18, 11 | oveq12d 7375 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
| 20 | | limcval.j |
. . . . . . . . 9
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
| 21 | 19, 20 | eqtr4di 2794 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = 𝐽) |
| 22 | 21, 18 | oveq12d 7375 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗) = (𝐽 CnP 𝐾)) |
| 23 | 22, 9 | fveq12d 6849 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗)‘𝑥) = ((𝐽 CnP 𝐾)‘𝐵)) |
| 24 | 15, 23 | eleq12d 2832 |
. . . . 5
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑧 ∈ (dom
𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 25 | 3, 24 | sbcied 3784 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
([(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 26 | 25 | abbidv 2805 |
. . 3
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) → {𝑦 ∣
[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)} = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 27 | | cnex 11132 |
. . . . 5
⊢ ℂ
∈ V |
| 28 | | elpm2r 8783 |
. . . . 5
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 29 | 27, 27, 28 | mpanl12 700 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 30 | 29 | 3adant3 1132 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 31 | | simp3 1138 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
| 32 | | eqid 2736 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 33 | 20, 17, 32 | limcvallem 25235 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝑦 ∈ ℂ)) |
| 34 | 33 | abssdv 4025 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ) |
| 35 | 27 | ssex 5278 |
. . . 4
⊢ ({𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 36 | 34, 35 | syl 17 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 37 | 2, 26, 30, 31, 36 | ovmpod 7507 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 38 | 37, 34 | eqsstrd 3982 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) ⊆ ℂ) |
| 39 | 37, 38 | jca 512 |
1
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) |
