| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-limc 24466 |
. . . 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 6687 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
(TopOpen‘ℂfld) ∈ V) |
| 4 | | simplrl 775 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑓 = 𝐹) |
| 5 | 4 | dmeqd 5776 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = dom 𝐹) |
| 6 | | simpll1 1208 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝐹:𝐴⟶ℂ) |
| 7 | 6 | fdmd 6525 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝐹 = 𝐴) |
| 8 | 5, 7 | eqtrd 2858 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ dom 𝑓 = 𝐴) |
| 9 | | simplrr 776 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑥 = 𝐵) |
| 10 | 9 | sneqd 4581 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ {𝑥} = {𝐵}) |
| 11 | 8, 10 | uneq12d 4142 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (dom 𝑓 ∪ {𝑥}) = (𝐴 ∪ {𝐵})) |
| 12 | 9 | eqeq2d 2834 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 = 𝑥 ↔ 𝑧 = 𝐵)) |
| 13 | 4 | fveq1d 6674 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑓‘𝑧) = (𝐹‘𝑧)) |
| 14 | 12, 13 | ifbieq2d 4494 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧)) = if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 15 | 11, 14 | mpteq12dv 5153 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧)))) |
| 16 | | simpr 487 |
. . . . . . . . . . 11
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 =
(TopOpen‘ℂfld)) |
| 17 | | limcval.k |
. . . . . . . . . . 11
⊢ 𝐾 =
(TopOpen‘ℂfld) |
| 18 | 16, 17 | syl6eqr 2876 |
. . . . . . . . . 10
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ 𝑗 = 𝐾) |
| 19 | 18, 11 | oveq12d 7176 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
| 20 | | limcval.j |
. . . . . . . . 9
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
| 21 | 19, 20 | syl6eqr 2876 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (𝑗
↾t (dom 𝑓
∪ {𝑥})) = 𝐽) |
| 22 | 21, 18 | oveq12d 7176 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗) = (𝐽 CnP 𝐾)) |
| 23 | 22, 9 | fveq12d 6679 |
. . . . . 6
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ (((𝑗
↾t (dom 𝑓
∪ {𝑥})) CnP 𝑗)‘𝑥) = ((𝐽 CnP 𝐾)‘𝐵)) |
| 24 | 15, 23 | eleq12d 2909 |
. . . . 5
⊢ ((((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) ∧ 𝑗 = (TopOpen‘ℂfld))
→ ((𝑧 ∈ (dom
𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 25 | 3, 24 | sbcied 3816 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) →
([(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
| 26 | 25 | abbidv 2887 |
. . 3
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑓 = 𝐹 ∧ 𝑥 = 𝐵)) → {𝑦 ∣
[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)} = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 27 | | cnex 10620 |
. . . . 5
⊢ ℂ
∈ V |
| 28 | | elpm2r 8426 |
. . . . 5
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 29 | 27, 27, 28 | mpanl12 700 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 30 | 29 | 3adant3 1128 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
| 31 | | simp3 1134 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ) |
| 32 | | eqid 2823 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) |
| 33 | 20, 17, 32 | limcvallem 24471 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝑦 ∈ ℂ)) |
| 34 | 33 | abssdv 4047 |
. . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ) |
| 35 | 27 | ssex 5227 |
. . . 4
⊢ ({𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ⊆ ℂ → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 36 | 34, 35 | syl 17 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∈ V) |
| 37 | 2, 26, 30, 31, 36 | ovmpod 7304 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)}) |
| 38 | 37, 34 | eqsstrd 4007 |
. 2
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐹 limℂ 𝐵) ⊆ ℂ) |
| 39 | 37, 38 | jca 514 |
1
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) |
