| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-limc 23436 |
. . . 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 | | fvex 6113 |
. . . . . 6
⊢
(TopOpen‘ℂfld) ∈ V |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
(TopOpen‘ℂfld) ∈ V) |
| 5 | | simplrl 796 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑓 = 𝐹) |
| 6 | 5 | dmeqd 5248 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = dom 𝐹) |
| 7 | | simpll1 1093 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝐹:𝐴⟶ℂ) |
| 8 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝐹 = 𝐴) |
| 10 | 6, 9 | eqtrd 2644 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = 𝐴) |
| 11 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑥 = 𝐵) |
| 12 | 11 | sneqd 4137 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ {𝑥} = {𝐵}) |
| 13 | 10, 12 | uneq12d 3730 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (dom 𝑓 ∪ {𝑥}) = (𝐴 ∪ {𝐵})) |
| 14 | 11 | eqeq2d 2620 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 = 𝑥 ↔ 𝑧 = 𝐵)) |
| 15 | 5 | fveq1d 6105 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑓‘𝑧) = (𝐹‘𝑧)) |
| 16 | 14, 15 | ifbieq2d 4061 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧)) = if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 17 | 13, 16 | mpteq12dv 4663 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧)))) |
| 18 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 =
(TopOpen‘ℂfld)) |
| 19 | | limcval.k |
. . . . . . . . . . 11
⊢ 𝐾 =
(TopOpen‘ℂfld) |
| 20 | 18, 19 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 = 𝐾) |
| 21 | 20, 13 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
| 22 | | limcval.j |
. . . . . . . . 9
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
| 23 | 21, 22 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = 𝐽) |
| 24 | 23, 20 | oveq12d 6567 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗) = (𝐽 CnP 𝐾)) |
| 25 | 24, 11 | fveq12d 6109 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗)‘𝑥) = ((𝐽 CnP 𝐾)‘𝐵)) |
| 26 | 17, 25 | eleq12d 2682 |
. . . . 5
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑧 ∈ (dom
𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 27 | 4, 26 | sbcied 3439 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
([(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 28 | 27 | abbidv 2728 |
. . 3
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) → {𝑦 ∣
[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)} = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 29 | | cnex 9896 |
. . . . 5
⊢ ℂ
∈ V |
| 30 | | elpm2r 7761 |
. . . . 5
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 31 | 29, 29, 30 | mpanl12 714 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 32 | 31 | 3adant3 1074 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 33 | | simp3 1056 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
| 34 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 35 | 22, 19, 34 | limcvallem 23441 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝑦 ∈ ℂ)) |
| 36 | 35 | abssdv 3639 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ) |
| 37 | 29 | ssex 4730 |
. . . 4
⊢ ({𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 38 | 36, 37 | syl 17 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 39 | 2, 28, 32, 33, 38 | ovmpt2d 6686 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 40 | 39, 36 | eqsstrd 3602 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) ⊆ ℂ) |
| 41 | 39, 40 | jca 553 |
1
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) |
