Step | Hyp | Ref
| Expression |
1 | | limccl 24772 |
. . 3
⊢ (𝐺 limℂ 𝐵) ⊆
ℂ |
2 | | limccog.3 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐵)) |
3 | 1, 2 | sseldi 3899 |
. 2
⊢ (𝜑 → 𝐶 ∈ ℂ) |
4 | | limcrcl 24771 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (𝐺 limℂ 𝐵) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
6 | 5 | simp1d 1144 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℂ) |
7 | 5 | simp2d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐺 ⊆ ℂ) |
8 | 5 | simp3d 1146 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
9 | | eqid 2737 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
10 | 6, 7, 8, 9 | ellimc2 24774 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ (𝐺 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢))))) |
11 | 2, 10 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)))) |
12 | 11 | simprd 499 |
. . . . . . 7
⊢ (𝜑 → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢))) |
13 | 12 | r19.21bi 3130 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢))) |
14 | 13 | imp 410 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) |
15 | | simp1ll 1238 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) → 𝜑) |
16 | | simp2 1139 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) → 𝑣 ∈
(TopOpen‘ℂfld)) |
17 | | simp3l 1203 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) → 𝐵 ∈ 𝑣) |
18 | | limccog.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ (𝐹 limℂ 𝐴)) |
19 | | limcrcl 24771 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ (𝐹 limℂ 𝐴) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐴 ∈ ℂ)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐴 ∈ ℂ)) |
21 | 20 | simp1d 1144 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
22 | 20 | simp2d 1145 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 ⊆ ℂ) |
23 | 20 | simp3d 1146 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℂ) |
24 | 21, 22, 23, 9 | ellimc2 24774 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∈ (𝐹 limℂ 𝐴) ↔ (𝐵 ∈ ℂ ∧ ∀𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣))))) |
25 | 18, 24 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣)))) |
26 | 25 | simprd 499 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣))) |
27 | 26 | r19.21bi 3130 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈
(TopOpen‘ℂfld)) → (𝐵 ∈ 𝑣 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣))) |
28 | 27 | imp 410 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈
(TopOpen‘ℂfld)) ∧ 𝐵 ∈ 𝑣) → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣)) |
29 | 15, 16, 17, 28 | syl21anc 838 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣)) |
30 | | imaco 6115 |
. . . . . . . . . . 11
⊢ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) = (𝐺 “ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴})))) |
31 | 15 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → 𝜑) |
32 | | simpl3r 1231 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) → (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) |
33 | 32 | adantr 484 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) |
34 | | simpr 488 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) |
35 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) |
36 | | imassrn 5940 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ ran 𝐹 |
37 | | limccog.1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ran 𝐹 ⊆ (dom 𝐺 ∖ {𝐵})) |
38 | 36, 37 | sstrid 3912 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ (dom 𝐺 ∖ {𝐵})) |
39 | 38 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ (dom 𝐺 ∖ {𝐵})) |
40 | 35, 39 | ssind 4147 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) |
41 | | imass2 5970 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ (𝑣 ∩ (dom 𝐺 ∖ {𝐵})) → (𝐺 “ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴})))) ⊆ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵})))) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐺 “ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴})))) ⊆ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵})))) |
43 | 42 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐺 “ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴})))) ⊆ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵})))) |
44 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) |
45 | 43, 44 | sstrd 3911 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐺 “ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴})))) ⊆ 𝑢) |
46 | 31, 33, 34, 45 | syl21anc 838 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐺 “ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴})))) ⊆ 𝑢) |
47 | 30, 46 | eqsstrid 3949 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢) |
48 | 47 | ex 416 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) → ((𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣 → ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢)) |
49 | 48 | anim2d 615 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) ∧ 𝑤 ∈
(TopOpen‘ℂfld)) → ((𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → (𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢))) |
50 | 49 | reximdva 3193 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) → (∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑣) → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢))) |
51 | 29, 50 | mpd 15 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ (𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢)) |
52 | 51 | rexlimdv3a 3205 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐺 “ (𝑣 ∩ (dom 𝐺 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢))) |
53 | 14, 52 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) ∧ 𝐶 ∈ 𝑢) → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢)) |
54 | 53 | ex 416 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (𝐶 ∈ 𝑢 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢))) |
55 | 54 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢))) |
56 | 21 | ffund 6549 |
. . . . . 6
⊢ (𝜑 → Fun 𝐹) |
57 | | fdmrn 6577 |
. . . . . 6
⊢ (Fun
𝐹 ↔ 𝐹:dom 𝐹⟶ran 𝐹) |
58 | 56, 57 | sylib 221 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶ran 𝐹) |
59 | 37 | difss2d 4049 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ dom 𝐺) |
60 | 58, 59 | fssd 6563 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶dom 𝐺) |
61 | | fco 6569 |
. . . 4
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝐹:dom 𝐹⟶dom 𝐺) → (𝐺 ∘ 𝐹):dom 𝐹⟶ℂ) |
62 | 6, 60, 61 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝐺 ∘ 𝐹):dom 𝐹⟶ℂ) |
63 | 62, 22, 23, 9 | ellimc2 24774 |
. 2
⊢ (𝜑 → (𝐶 ∈ ((𝐺 ∘ 𝐹) limℂ 𝐴) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑤 ∈
(TopOpen‘ℂfld)(𝐴 ∈ 𝑤 ∧ ((𝐺 ∘ 𝐹) “ (𝑤 ∩ (dom 𝐹 ∖ {𝐴}))) ⊆ 𝑢))))) |
64 | 3, 55, 63 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐶 ∈ ((𝐺 ∘ 𝐹) limℂ 𝐴)) |