| Step | Hyp | Ref
| Expression |
| 1 | | limcrcl 25909 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
| 2 | 1 | simp1d 1143 |
. . . . . 6
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝐹:dom 𝐹⟶ℂ) |
| 3 | 1 | simp2d 1144 |
. . . . . 6
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → dom 𝐹 ⊆ ℂ) |
| 4 | 1 | simp3d 1145 |
. . . . . 6
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝐵 ∈ ℂ) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 6 | 2, 3, 4, 5 | ellimc2 25912 |
. . . . 5
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢))))) |
| 7 | 6 | ibi 267 |
. . . 4
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝑥 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢)))) |
| 8 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵})) ⊆ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}) |
| 9 | | difss 4136 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝐹 ∩ 𝐶) ∖ {𝐵}) ⊆ (dom 𝐹 ∩ 𝐶) |
| 10 | | inss2 4238 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐹 ∩ 𝐶) ⊆ 𝐶 |
| 11 | 9, 10 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∩ 𝐶) ∖ {𝐵}) ⊆ 𝐶 |
| 12 | 8, 11 | sstri 3993 |
. . . . . . . . . . . 12
⊢ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵})) ⊆ 𝐶 |
| 13 | | resima2 6034 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵})) ⊆ 𝐶 → ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) = (𝐹 “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵})))) |
| 14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) = (𝐹 “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) |
| 15 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (dom
𝐹 ∩ 𝐶) ⊆ dom 𝐹 |
| 16 | | ssdif 4144 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∩ 𝐶) ⊆ dom 𝐹 → ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}) ⊆ (dom 𝐹 ∖ {𝐵})) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((dom
𝐹 ∩ 𝐶) ∖ {𝐵}) ⊆ (dom 𝐹 ∖ {𝐵}) |
| 18 | | sslin 4243 |
. . . . . . . . . . . 12
⊢ (((dom
𝐹 ∩ 𝐶) ∖ {𝐵}) ⊆ (dom 𝐹 ∖ {𝐵}) → (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵})) ⊆ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) |
| 19 | | imass2 6120 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵})) ⊆ (𝑣 ∩ (dom 𝐹 ∖ {𝐵})) → (𝐹 “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵})))) |
| 20 | 17, 18, 19 | mp2b 10 |
. . . . . . . . . . 11
⊢ (𝐹 “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) |
| 21 | 14, 20 | eqsstri 4030 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) |
| 22 | | sstr 3992 |
. . . . . . . . . 10
⊢ ((((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢) → ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢) |
| 23 | 21, 22 | mpan 690 |
. . . . . . . . 9
⊢ ((𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢 → ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢) |
| 24 | 23 | anim2i 617 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢) → (𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢)) |
| 25 | 24 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢)) |
| 26 | 25 | imim2i 16 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢)) → (𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢))) |
| 27 | 26 | ralimi 3083 |
. . . . 5
⊢
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢))) |
| 28 | 27 | anim2i 617 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧
∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (dom 𝐹 ∖ {𝐵}))) ⊆ 𝑢))) → (𝑥 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢)))) |
| 29 | 7, 28 | syl 17 |
. . 3
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝑥 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢)))) |
| 30 | | fresin 6777 |
. . . . 5
⊢ (𝐹:dom 𝐹⟶ℂ → (𝐹 ↾ 𝐶):(dom 𝐹 ∩ 𝐶)⟶ℂ) |
| 31 | 2, 30 | syl 17 |
. . . 4
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐹 ↾ 𝐶):(dom 𝐹 ∩ 𝐶)⟶ℂ) |
| 32 | 15, 3 | sstrid 3995 |
. . . 4
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (dom 𝐹 ∩ 𝐶) ⊆ ℂ) |
| 33 | 31, 32, 4, 5 | ellimc2 25912 |
. . 3
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑥 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ ((𝐹 ↾ 𝐶) “ (𝑣 ∩ ((dom 𝐹 ∩ 𝐶) ∖ {𝐵}))) ⊆ 𝑢))))) |
| 34 | 29, 33 | mpbird 257 |
. 2
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵)) |
| 35 | 34 | ssriv 3987 |
1
⊢ (𝐹 limℂ 𝐵) ⊆ ((𝐹 ↾ 𝐶) limℂ 𝐵) |