Step | Hyp | Ref
| Expression |
1 | | limccl 25037 |
. . . 4
⊢ (𝐹 limℂ 𝐶) ⊆
ℂ |
2 | | limcresi 25047 |
. . . . . 6
⊢ (𝐹 limℂ 𝐶) ⊆ ((𝐹 ↾ 𝐵) limℂ 𝐶) |
3 | 2 | rgenw 3078 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 (𝐹 limℂ 𝐶) ⊆ ((𝐹 ↾ 𝐵) limℂ 𝐶) |
4 | | ssiin 4990 |
. . . . 5
⊢ ((𝐹 limℂ 𝐶) ⊆ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶) ↔ ∀𝑥 ∈ 𝐴 (𝐹 limℂ 𝐶) ⊆ ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
5 | 3, 4 | mpbir 230 |
. . . 4
⊢ (𝐹 limℂ 𝐶) ⊆ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶) |
6 | 1, 5 | ssini 4171 |
. . 3
⊢ (𝐹 limℂ 𝐶) ⊆ (ℂ ∩
∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹 limℂ 𝐶) ⊆ (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
8 | | elriin 5015 |
. . . 4
⊢ (𝑦 ∈ (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) ↔ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
9 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝑦 ∈ ℂ) |
10 | | limciun.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ Fin) |
11 | 10 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → 𝐴 ∈ Fin) |
12 | | simplrr 775 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
13 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐹 |
14 | | nfcsb1v 3862 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐵 |
15 | 13, 14 | nfres 5892 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) |
16 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥
limℂ |
17 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐶 |
18 | 15, 16, 17 | nfov 7301 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) |
19 | 18 | nfcri 2896 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) |
20 | | csbeq1a 3851 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑥⦌𝐵) |
21 | 20 | reseq2d 5890 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝐹 ↾ 𝐵) = (𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵)) |
22 | 21 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((𝐹 ↾ 𝐵) limℂ 𝐶) = ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶)) |
23 | 22 | eleq2d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶) ↔ 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶))) |
24 | 19, 23 | rspc 3548 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶) → 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶))) |
25 | 12, 24 | mpan9 507 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶)) |
26 | | limciun.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) |
27 | 26 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) |
28 | | ssiun2 4982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝐴 → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ∪
𝑎 ∈ 𝐴 ⦋𝑎 / 𝑥⦌𝐵) |
29 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎𝐵 |
30 | 29, 14, 20 | cbviun 4971 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑎 ∈ 𝐴 ⦋𝑎 / 𝑥⦌𝐵 |
31 | 28, 30 | sseqtrrdi 3977 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝐴 → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
33 | 27, 32 | fssresd 6639 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → (𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵):⦋𝑎 / 𝑥⦌𝐵⟶ℂ) |
34 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
35 | | limciun.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
36 | 35 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
37 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥ℂ |
38 | 14, 37 | nfss 3918 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ |
39 | 20 | sseq1d 3957 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝐵 ⊆ ℂ ↔ ⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ)) |
40 | 38, 39 | rspc 3548 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ)) |
41 | 34, 36, 40 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ) |
42 | | limciun.4 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ℂ) |
43 | 42 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ ℂ) |
44 | | eqid 2740 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
45 | 33, 41, 43, 44 | ellimc2 25039 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → (𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))))) |
46 | 45 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → (𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))))) |
47 | 25, 46 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)))) |
48 | 47 | simprd 496 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
49 | | simplrl 774 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → 𝑢 ∈
(TopOpen‘ℂfld)) |
50 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → 𝑦 ∈ 𝑢) |
51 | | rsp 3132 |
. . . . . . . . . . . . 13
⊢
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → (𝑢 ∈ (TopOpen‘ℂfld)
→ (𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)))) |
52 | 48, 49, 50, 51 | syl3c 66 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
53 | 52 | ralrimiva 3110 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∀𝑎 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
54 | | nfv 1921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
55 | | nfcv 2909 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(TopOpen‘ℂfld) |
56 | | nfv 1921 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥 𝐶 ∈ 𝑘 |
57 | | nfcv 2909 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝑘 |
58 | | nfcv 2909 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥{𝐶} |
59 | 14, 58 | nfdif 4065 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}) |
60 | 57, 59 | nfin 4156 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶})) |
61 | 15, 60 | nfima 5976 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) |
62 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝑢 |
63 | 61, 62 | nfss 3918 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢 |
64 | 56, 63 | nfan 1906 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
65 | 55, 64 | nfrex 3240 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
66 | 20 | difeq1d 4061 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝐵 ∖ {𝐶}) = (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶})) |
67 | 66 | ineq2d 4152 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑘 ∩ (𝐵 ∖ {𝐶})) = (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) |
68 | 21, 67 | imaeq12d 5969 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶})))) |
69 | 68 | sseq1d 3957 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
70 | 69 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → ((𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
71 | 70 | rexbidv 3228 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
72 | 54, 65, 71 | cbvralw 3372 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∀𝑎 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
73 | 53, 72 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∀𝑥 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
74 | | eleq2 2829 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑔‘𝑥) → (𝐶 ∈ 𝑘 ↔ 𝐶 ∈ (𝑔‘𝑥))) |
75 | | ineq1 4145 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑔‘𝑥) → (𝑘 ∩ (𝐵 ∖ {𝐶})) = ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) |
76 | 75 | imaeq2d 5968 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑔‘𝑥) → ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶})))) |
77 | 76 | sseq1d 3957 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑔‘𝑥) → (((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
78 | 74, 77 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑔‘𝑥) → ((𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
79 | 78 | ac6sfi 9036 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
80 | 11, 73, 79 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
81 | 44 | cnfldtop 23945 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) ∈ Top |
82 | | frn 6605 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐴⟶(TopOpen‘ℂfld)
→ ran 𝑔 ⊆
(TopOpen‘ℂfld)) |
83 | 82 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ⊆
(TopOpen‘ℂfld)) |
84 | 11 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐴 ∈ Fin) |
85 | | ffn 6598 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝐴⟶(TopOpen‘ℂfld)
→ 𝑔 Fn 𝐴) |
86 | 85 | ad2antrl 725 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔 Fn 𝐴) |
87 | | dffn4 6692 |
. . . . . . . . . . . . 13
⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–onto→ran 𝑔) |
88 | 86, 87 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔:𝐴–onto→ran 𝑔) |
89 | | fofi 9083 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑔:𝐴–onto→ran 𝑔) → ran 𝑔 ∈ Fin) |
90 | 84, 88, 89 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ∈ Fin) |
91 | | unicntop 23947 |
. . . . . . . . . . . 12
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
92 | 91 | rintopn 22056 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ran 𝑔 ⊆
(TopOpen‘ℂfld) ∧ ran 𝑔 ∈ Fin) → (ℂ ∩ ∩ ran 𝑔) ∈
(TopOpen‘ℂfld)) |
93 | 81, 83, 90, 92 | mp3an2i 1465 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (ℂ ∩ ∩ ran 𝑔) ∈
(TopOpen‘ℂfld)) |
94 | 42 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝐶 ∈ ℂ) |
95 | 94 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ ℂ) |
96 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → 𝐶 ∈ (𝑔‘𝑥)) |
97 | 96 | ralimi 3089 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥)) |
98 | 97 | ad2antll 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥)) |
99 | | eleq2 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑔‘𝑥) → (𝐶 ∈ 𝑧 ↔ 𝐶 ∈ (𝑔‘𝑥))) |
100 | 99 | ralrn 6961 |
. . . . . . . . . . . . 13
⊢ (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥))) |
101 | 86, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥))) |
102 | 98, 101 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧) |
103 | | elrint 4928 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (ℂ ∩ ∩ ran 𝑔) ↔ (𝐶 ∈ ℂ ∧ ∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧)) |
104 | 95, 102, 103 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ (ℂ ∩ ∩ ran 𝑔)) |
105 | | indifcom 4212 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})) = (∪
𝑥 ∈ 𝐴 𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) |
106 | | iunin1 5006 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) = (∪
𝑥 ∈ 𝐴 𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) |
107 | 105, 106 | eqtr4i 2771 |
. . . . . . . . . . . . 13
⊢ ((ℂ
∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})) = ∪
𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) |
108 | 107 | imaeq2i 5966 |
. . . . . . . . . . . 12
⊢ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) = (𝐹 “ ∪
𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) |
109 | | imaiun 7115 |
. . . . . . . . . . . 12
⊢ (𝐹 “ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) = ∪
𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) |
110 | 108, 109 | eqtri 2768 |
. . . . . . . . . . 11
⊢ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) = ∪
𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) |
111 | | inss2 4169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℂ
∩ ∩ ran 𝑔) ⊆ ∩ ran
𝑔 |
112 | | fnfvelrn 6955 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) |
113 | 85, 112 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) |
114 | | intss1 4900 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔‘𝑥) ∈ ran 𝑔 → ∩ ran
𝑔 ⊆ (𝑔‘𝑥)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → ∩ ran 𝑔
⊆ (𝑔‘𝑥)) |
116 | 111, 115 | sstrid 3937 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (ℂ ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑥)) |
117 | 116 | ssdifd 4080 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔‘𝑥) ∖ {𝐶})) |
118 | | sslin 4174 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔‘𝑥) ∖ {𝐶}) → (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
119 | | imass2 6009 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})))) |
120 | 117, 118,
119 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})))) |
121 | | indifcom 4212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶})) = (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) |
122 | 121 | imaeq2i 5966 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) = ((𝐹 ↾ 𝐵) “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
123 | | inss1 4168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) ⊆ 𝐵 |
124 | | resima2 5925 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})))) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ 𝐵) “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
126 | 122, 125 | eqtri 2768 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
127 | 120, 126 | sseqtrrdi 3977 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶})))) |
128 | | sstr2 3933 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) → (((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
130 | 129 | adantld 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → ((𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
131 | 130 | ralimdva 3105 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝐴⟶(TopOpen‘ℂfld)
→ (∀𝑥 ∈
𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
132 | 131 | imp 407 |
. . . . . . . . . . . . 13
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
133 | 132 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
134 | | iunss 4980 |
. . . . . . . . . . . 12
⊢ (∪ 𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢 ↔ ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
135 | 133, 134 | sylibr 233 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∪
𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
136 | 110, 135 | eqsstrid 3974 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
137 | | eleq2 2829 |
. . . . . . . . . . . 12
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → (𝐶 ∈ 𝑣 ↔ 𝐶 ∈ (ℂ ∩ ∩ ran 𝑔))) |
138 | | ineq1 4145 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})) = ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) |
139 | 138 | imaeq2d 5968 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) = (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})))) |
140 | 139 | sseq1d 3957 |
. . . . . . . . . . . 12
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → ((𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
141 | 137, 140 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → ((𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (ℂ ∩ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
142 | 141 | rspcev 3561 |
. . . . . . . . . 10
⊢
(((ℂ ∩ ∩ ran 𝑔) ∈
(TopOpen‘ℂfld) ∧ (𝐶 ∈ (ℂ ∩ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
143 | 93, 104, 136, 142 | syl12anc 834 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
144 | 80, 143 | exlimddv 1942 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
145 | 144 | expr 457 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (𝑦 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
146 | 145 | ralrimiva 3110 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
147 | 26 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) |
148 | | iunss 4980 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
149 | 35, 148 | sylibr 233 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
150 | 149 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
151 | 147, 150,
94, 44 | ellimc2 25039 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → (𝑦 ∈ (𝐹 limℂ 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))))) |
152 | 9, 146, 151 | mpbir2and 710 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝑦 ∈ (𝐹 limℂ 𝐶)) |
153 | 152 | ex 413 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑦 ∈ (𝐹 limℂ 𝐶))) |
154 | 8, 153 | syl5bi 241 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑦 ∈ (𝐹 limℂ 𝐶))) |
155 | 154 | ssrdv 3932 |
. 2
⊢ (𝜑 → (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) ⊆ (𝐹 limℂ 𝐶)) |
156 | 7, 155 | eqssd 3943 |
1
⊢ (𝜑 → (𝐹 limℂ 𝐶) = (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶))) |