Step | Hyp | Ref
| Expression |
1 | | limccl 23445 |
. . . 4
⊢ (𝐹 limℂ 𝐶) ⊆
ℂ |
2 | | limcresi 23455 |
. . . . . 6
⊢ (𝐹 limℂ 𝐶) ⊆ ((𝐹 ↾ 𝐵) limℂ 𝐶) |
3 | 2 | rgenw 2908 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 (𝐹 limℂ 𝐶) ⊆ ((𝐹 ↾ 𝐵) limℂ 𝐶) |
4 | | ssiin 4506 |
. . . . 5
⊢ ((𝐹 limℂ 𝐶) ⊆ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶) ↔ ∀𝑥 ∈ 𝐴 (𝐹 limℂ 𝐶) ⊆ ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
5 | 3, 4 | mpbir 220 |
. . . 4
⊢ (𝐹 limℂ 𝐶) ⊆ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶) |
6 | 1, 5 | ssini 3798 |
. . 3
⊢ (𝐹 limℂ 𝐶) ⊆ (ℂ ∩
∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹 limℂ 𝐶) ⊆ (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
8 | | elriin 4529 |
. . . 4
⊢ (𝑦 ∈ (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) ↔ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
9 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝑦 ∈ ℂ) |
10 | | limciun.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ Fin) |
11 | 10 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → 𝐴 ∈ Fin) |
12 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
13 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥𝐹 |
14 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐵 |
15 | 13, 14 | nfres 5319 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) |
16 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥
limℂ |
17 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐶 |
18 | 15, 16, 17 | nfov 6575 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) |
19 | 18 | nfcri 2745 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) |
20 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑥⦌𝐵) |
21 | 20 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝐹 ↾ 𝐵) = (𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵)) |
22 | 21 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((𝐹 ↾ 𝐵) limℂ 𝐶) = ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶)) |
23 | 22 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶) ↔ 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶))) |
24 | 19, 23 | rspc 3276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶) → 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶))) |
25 | 12, 24 | mpan9 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → 𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶)) |
26 | | limciun.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) |
27 | 26 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) |
28 | | ssiun2 4499 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝐴 → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ∪
𝑎 ∈ 𝐴 ⦋𝑎 / 𝑥⦌𝐵) |
29 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎𝐵 |
30 | 29, 14, 20 | cbviun 4493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑎 ∈ 𝐴 ⦋𝑎 / 𝑥⦌𝐵 |
31 | 28, 30 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝐴 → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
33 | 27, 32 | fssresd 5984 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → (𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵):⦋𝑎 / 𝑥⦌𝐵⟶ℂ) |
34 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
35 | | limciun.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
36 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
37 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥ℂ |
38 | 14, 37 | nfss 3561 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ |
39 | 20 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝐵 ⊆ ℂ ↔ ⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ)) |
40 | 38, 39 | rspc 3276 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ)) |
41 | 34, 36, 40 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → ⦋𝑎 / 𝑥⦌𝐵 ⊆ ℂ) |
42 | | limciun.4 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ℂ) |
43 | 42 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → 𝐶 ∈ ℂ) |
44 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
45 | 33, 41, 43, 44 | ellimc2 23447 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑎 ∈ 𝐴) → (𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))))) |
46 | 45 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → (𝑦 ∈ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) limℂ 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))))) |
47 | 25, 46 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)))) |
48 | 47 | simprd 478 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
49 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → 𝑢 ∈
(TopOpen‘ℂfld)) |
50 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → 𝑦 ∈ 𝑢) |
51 | | rsp 2913 |
. . . . . . . . . . . . 13
⊢
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → (𝑢 ∈ (TopOpen‘ℂfld)
→ (𝑦 ∈ 𝑢 → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)))) |
52 | 48, 49, 50, 51 | syl3c 64 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ 𝑎 ∈ 𝐴) → ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
53 | 52 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∀𝑎 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
54 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑎∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
55 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(TopOpen‘ℂfld) |
56 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥 𝐶 ∈ 𝑘 |
57 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝑘 |
58 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥{𝐶} |
59 | 14, 58 | nfdif 3693 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}) |
60 | 57, 59 | nfin 3782 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶})) |
61 | 15, 60 | nfima 5393 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) |
62 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝑢 |
63 | 61, 62 | nfss 3561 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢 |
64 | 56, 63 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
65 | 55, 64 | nfrex 2990 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
66 | 20 | difeq1d 3689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝐵 ∖ {𝐶}) = (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶})) |
67 | 66 | ineq2d 3776 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑘 ∩ (𝐵 ∖ {𝐶})) = (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) |
68 | 21, 67 | imaeq12d 5386 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶})))) |
69 | 68 | sseq1d 3595 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
70 | 69 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → ((𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
71 | 70 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
72 | 54, 65, 71 | cbvral 3143 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∀𝑎 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ ⦋𝑎 / 𝑥⦌𝐵) “ (𝑘 ∩ (⦋𝑎 / 𝑥⦌𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
73 | 53, 72 | sylibr 223 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∀𝑥 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
74 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑔‘𝑥) → (𝐶 ∈ 𝑘 ↔ 𝐶 ∈ (𝑔‘𝑥))) |
75 | | ineq1 3769 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑔‘𝑥) → (𝑘 ∩ (𝐵 ∖ {𝐶})) = ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) |
76 | 75 | imaeq2d 5385 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑔‘𝑥) → ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶})))) |
77 | 76 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑔‘𝑥) → (((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
78 | 74, 77 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑔‘𝑥) → ((𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
79 | 78 | ac6sfi 8089 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑘 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑘 ∧ ((𝐹 ↾ 𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
80 | 11, 73, 79 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
81 | 44 | cnfldtop 22397 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈ Top |
82 | 81 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) →
(TopOpen‘ℂfld) ∈ Top) |
83 | | frn 5966 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐴⟶(TopOpen‘ℂfld)
→ ran 𝑔 ⊆
(TopOpen‘ℂfld)) |
84 | 83 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ⊆
(TopOpen‘ℂfld)) |
85 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐴 ∈ Fin) |
86 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝐴⟶(TopOpen‘ℂfld)
→ 𝑔 Fn 𝐴) |
87 | 86 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔 Fn 𝐴) |
88 | | dffn4 6034 |
. . . . . . . . . . . . 13
⊢ (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–onto→ran 𝑔) |
89 | 87, 88 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔:𝐴–onto→ran 𝑔) |
90 | | fofi 8135 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑔:𝐴–onto→ran 𝑔) → ran 𝑔 ∈ Fin) |
91 | 85, 89, 90 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ∈ Fin) |
92 | 44 | cnfldtopon 22396 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
93 | 92 | toponunii 20547 |
. . . . . . . . . . . 12
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
94 | 93 | rintopn 20539 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ran 𝑔 ⊆
(TopOpen‘ℂfld) ∧ ran 𝑔 ∈ Fin) → (ℂ ∩ ∩ ran 𝑔) ∈
(TopOpen‘ℂfld)) |
95 | 82, 84, 91, 94 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (ℂ ∩ ∩ ran 𝑔) ∈
(TopOpen‘ℂfld)) |
96 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝐶 ∈ ℂ) |
97 | 96 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ ℂ) |
98 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → 𝐶 ∈ (𝑔‘𝑥)) |
99 | 98 | ralimi 2936 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥)) |
100 | 99 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥)) |
101 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑔‘𝑥) → (𝐶 ∈ 𝑧 ↔ 𝐶 ∈ (𝑔‘𝑥))) |
102 | 101 | ralrn 6270 |
. . . . . . . . . . . . 13
⊢ (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥))) |
103 | 87, 102 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ (𝑔‘𝑥))) |
104 | 100, 103 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧) |
105 | | elrint 4453 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (ℂ ∩ ∩ ran 𝑔) ↔ (𝐶 ∈ ℂ ∧ ∀𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧)) |
106 | 97, 104, 105 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ (ℂ ∩ ∩ ran 𝑔)) |
107 | | indifcom 3831 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})) = (∪
𝑥 ∈ 𝐴 𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) |
108 | | iunin1 4521 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) = (∪
𝑥 ∈ 𝐴 𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) |
109 | 107, 108 | eqtr4i 2635 |
. . . . . . . . . . . . 13
⊢ ((ℂ
∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})) = ∪
𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) |
110 | 109 | imaeq2i 5383 |
. . . . . . . . . . . 12
⊢ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) = (𝐹 “ ∪
𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) |
111 | | imaiun 6407 |
. . . . . . . . . . . 12
⊢ (𝐹 “ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) = ∪
𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) |
112 | 110, 111 | eqtri 2632 |
. . . . . . . . . . 11
⊢ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) = ∪
𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) |
113 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℂ
∩ ∩ ran 𝑔) ⊆ ∩ ran
𝑔 |
114 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) |
115 | 86, 114 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (𝑔‘𝑥) ∈ ran 𝑔) |
116 | | intss1 4427 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔‘𝑥) ∈ ran 𝑔 → ∩ ran
𝑔 ⊆ (𝑔‘𝑥)) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → ∩ ran 𝑔
⊆ (𝑔‘𝑥)) |
118 | 113, 117 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (ℂ ∩ ∩ ran 𝑔) ⊆ (𝑔‘𝑥)) |
119 | 118 | ssdifd 3708 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔‘𝑥) ∖ {𝐶})) |
120 | | sslin 3801 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔‘𝑥) ∖ {𝐶}) → (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
121 | | imass2 5420 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})))) |
122 | 119, 120,
121 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})))) |
123 | | indifcom 3831 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶})) = (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) |
124 | 123 | imaeq2i 5383 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) = ((𝐹 ↾ 𝐵) “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
125 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) ⊆ 𝐵 |
126 | | resima2 5352 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶})))) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ 𝐵) “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
128 | 124, 127 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔‘𝑥) ∖ {𝐶}))) |
129 | 122, 128 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶})))) |
130 | | sstr2 3575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) → (((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → (((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
132 | 131 | adantld 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ 𝑥 ∈ 𝐴) → ((𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
133 | 132 | ralimdva 2945 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝐴⟶(TopOpen‘ℂfld)
→ (∀𝑥 ∈
𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)) |
134 | 133 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
135 | 134 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
136 | | iunss 4497 |
. . . . . . . . . . . 12
⊢ (∪ 𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢 ↔ ∀𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
137 | 135, 136 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∪
𝑥 ∈ 𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢) |
138 | 112, 137 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢) |
139 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → (𝐶 ∈ 𝑣 ↔ 𝐶 ∈ (ℂ ∩ ∩ ran 𝑔))) |
140 | | ineq1 3769 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})) = ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) |
141 | 140 | imaeq2d 5385 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) = (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶})))) |
142 | 141 | sseq1d 3595 |
. . . . . . . . . . . 12
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → ((𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
143 | 139, 142 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑣 = (ℂ ∩ ∩ ran 𝑔) → ((𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (ℂ ∩ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
144 | 143 | rspcev 3282 |
. . . . . . . . . 10
⊢
(((ℂ ∩ ∩ ran 𝑔) ∈
(TopOpen‘ℂfld) ∧ (𝐶 ∈ (ℂ ∩ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ∩ ran 𝑔) ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
145 | 95, 106, 138, 144 | syl12anc 1316 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld)
∧ ∀𝑥 ∈ 𝐴 (𝐶 ∈ (𝑔‘𝑥) ∧ ((𝐹 ↾ 𝐵) “ ((𝑔‘𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
146 | 80, 145 | exlimddv 1850 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝑦 ∈ 𝑢)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) |
147 | 146 | expr 641 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (𝑦 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
148 | 147 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))) |
149 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶ℂ) |
150 | | iunss 4497 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
151 | 35, 150 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
152 | 151 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ) |
153 | 149, 152,
96, 44 | ellimc2 23447 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → (𝑦 ∈ (𝐹 limℂ 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝑦 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (∪
𝑥 ∈ 𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))))) |
154 | 9, 148, 153 | mpbir2and 959 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) → 𝑦 ∈ (𝐹 limℂ 𝐶)) |
155 | 154 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℂ ∧ ∀𝑥 ∈ 𝐴 𝑦 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑦 ∈ (𝐹 limℂ 𝐶))) |
156 | 8, 155 | syl5bi 231 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑦 ∈ (𝐹 limℂ 𝐶))) |
157 | 156 | ssrdv 3574 |
. 2
⊢ (𝜑 → (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶)) ⊆ (𝐹 limℂ 𝐶)) |
158 | 7, 157 | eqssd 3585 |
1
⊢ (𝜑 → (𝐹 limℂ 𝐶) = (ℂ ∩ ∩ 𝑥 ∈ 𝐴 ((𝐹 ↾ 𝐵) limℂ 𝐶))) |