Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
2 | 1 | inex1 4799 |
. . . . . . . . . 10
⊢ (𝑡 ∩ 𝐶) ∈ V |
3 | 2 | rgenw 2924 |
. . . . . . . . 9
⊢
∀𝑡 ∈
((nei‘𝐾)‘{𝐵})(𝑡 ∩ 𝐶) ∈ V |
4 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶)) = (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶)) |
5 | | imaeq2 5462 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑡 ∩ 𝐶) → ((𝐹 ↾ 𝐶) “ 𝑠) = ((𝐹 ↾ 𝐶) “ (𝑡 ∩ 𝐶))) |
6 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∩ 𝐶) ⊆ 𝐶 |
7 | | resima2 5432 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∩ 𝐶) ⊆ 𝐶 → ((𝐹 ↾ 𝐶) “ (𝑡 ∩ 𝐶)) = (𝐹 “ (𝑡 ∩ 𝐶))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ 𝐶) “ (𝑡 ∩ 𝐶)) = (𝐹 “ (𝑡 ∩ 𝐶)) |
9 | 5, 8 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝑡 ∩ 𝐶) → ((𝐹 ↾ 𝐶) “ 𝑠) = (𝐹 “ (𝑡 ∩ 𝐶))) |
10 | 9 | sseq1d 3632 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑡 ∩ 𝐶) → (((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) |
11 | 4, 10 | rexrnmpt 6369 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
((nei‘𝐾)‘{𝐵})(𝑡 ∩ 𝐶) ∈ V → (∃𝑠 ∈ ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) |
12 | 3, 11 | mp1i 13 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑠 ∈ ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) |
13 | | limcflf.l |
. . . . . . . . . 10
⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) |
14 | | fvex 6201 |
. . . . . . . . . . 11
⊢
((nei‘𝐾)‘{𝐵}) ∈ V |
15 | | limcflf.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (𝐴 ∖ {𝐵}) |
16 | | difss 3737 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
17 | 15, 16 | eqsstri 3635 |
. . . . . . . . . . . . . 14
⊢ 𝐶 ⊆ 𝐴 |
18 | | limcflf.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
19 | 17, 18 | syl5ss 3614 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ⊆ ℂ) |
20 | | cnex 10017 |
. . . . . . . . . . . . . 14
⊢ ℂ
∈ V |
21 | 20 | ssex 4802 |
. . . . . . . . . . . . 13
⊢ (𝐶 ⊆ ℂ → 𝐶 ∈ V) |
22 | 19, 21 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ V) |
23 | 22 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → 𝐶 ∈ V) |
24 | | restval 16087 |
. . . . . . . . . . 11
⊢
((((nei‘𝐾)‘{𝐵}) ∈ V ∧ 𝐶 ∈ V) → (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) = ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))) |
25 | 14, 23, 24 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) = ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))) |
26 | 13, 25 | syl5eq 2668 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → 𝐿 = ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))) |
27 | 26 | rexeqdv 3145 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ ∃𝑠 ∈ ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)) |
28 | | limcflf.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 =
(TopOpen‘ℂfld) |
29 | 28 | cnfldtop 22587 |
. . . . . . . . . . . . 13
⊢ 𝐾 ∈ Top |
30 | | opnneip 20923 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤) → 𝑤 ∈ ((nei‘𝐾)‘{𝐵})) |
31 | 29, 30 | mp3an1 1411 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤) → 𝑤 ∈ ((nei‘𝐾)‘{𝐵})) |
32 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤) |
33 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑤 → 𝐶 = (𝐴 ∖ {𝐵})) |
34 | 32, 33 | ineq12d 3815 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑤 → (𝑡 ∩ 𝐶) = (𝑤 ∩ (𝐴 ∖ {𝐵}))) |
35 | 34 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑤 → (𝐹 “ (𝑡 ∩ 𝐶)) = (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵})))) |
36 | 35 | sseq1d 3632 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑤 → ((𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢 ↔ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
37 | 36 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) |
38 | 31, 37 | sylan 488 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤) ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) |
39 | 38 | anasss 679 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝐾 ∧ (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) |
40 | 39 | rexlimiva 3028 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) |
41 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝑡 ∈ ((nei‘𝐾)‘{𝐵})) |
42 | 28 | cnfldtopon 22586 |
. . . . . . . . . . . . . . 15
⊢ 𝐾 ∈
(TopOn‘ℂ) |
43 | 42 | toponunii 20721 |
. . . . . . . . . . . . . 14
⊢ ℂ =
∪ 𝐾 |
44 | 43 | neii1 20910 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑡 ∈ ((nei‘𝐾)‘{𝐵})) → 𝑡 ⊆ ℂ) |
45 | 29, 41, 44 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝑡 ⊆ ℂ) |
46 | 43 | ntropn 20853 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Top ∧ 𝑡 ⊆ ℂ) →
((int‘𝐾)‘𝑡) ∈ 𝐾) |
47 | 29, 45, 46 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → ((int‘𝐾)‘𝑡) ∈ 𝐾) |
48 | 29 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝐾 ∈ Top) |
49 | 43 | lpss 20946 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Top ∧ 𝐴 ⊆ ℂ) →
((limPt‘𝐾)‘𝐴) ⊆ ℂ) |
50 | 29, 18, 49 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((limPt‘𝐾)‘𝐴) ⊆ ℂ) |
51 | | limcflf.b |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) |
52 | 50, 51 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℂ) |
53 | 52 | snssd 4340 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝐵} ⊆ ℂ) |
54 | 53 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → {𝐵} ⊆ ℂ) |
55 | 43 | neiint 20908 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ {𝐵} ⊆ ℂ ∧ 𝑡 ⊆ ℂ) → (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) |
56 | 48, 54, 45, 55 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) |
57 | 41, 56 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → {𝐵} ⊆ ((int‘𝐾)‘𝑡)) |
58 | 52 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝐵 ∈ ℂ) |
59 | | snssg 4327 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℂ → (𝐵 ∈ ((int‘𝐾)‘𝑡) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐵 ∈ ((int‘𝐾)‘𝑡) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) |
61 | 57, 60 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝐵 ∈ ((int‘𝐾)‘𝑡)) |
62 | 43 | ntrss2 20861 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ 𝑡 ⊆ ℂ) →
((int‘𝐾)‘𝑡) ⊆ 𝑡) |
63 | 29, 45, 62 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → ((int‘𝐾)‘𝑡) ⊆ 𝑡) |
64 | | ssrin 3838 |
. . . . . . . . . . . . 13
⊢
(((int‘𝐾)‘𝑡) ⊆ 𝑡 → (((int‘𝐾)‘𝑡) ∩ 𝐶) ⊆ (𝑡 ∩ 𝐶)) |
65 | | imass2 5501 |
. . . . . . . . . . . . 13
⊢
((((int‘𝐾)‘𝑡) ∩ 𝐶) ⊆ (𝑡 ∩ 𝐶) → (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ (𝐹 “ (𝑡 ∩ 𝐶))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ (𝐹 “ (𝑡 ∩ 𝐶))) |
67 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) |
68 | 66, 67 | sstrd 3613 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢) |
69 | | eleq2 2690 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝐵 ∈ 𝑤 ↔ 𝐵 ∈ ((int‘𝐾)‘𝑡))) |
70 | 15 | ineq2i 3811 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∩ 𝐶) = (𝑤 ∩ (𝐴 ∖ {𝐵})) |
71 | | ineq1 3807 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝑤 ∩ 𝐶) = (((int‘𝐾)‘𝑡) ∩ 𝐶)) |
72 | 70, 71 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝑤 ∩ (𝐴 ∖ {𝐵})) = (((int‘𝐾)‘𝑡) ∩ 𝐶)) |
73 | 72 | imaeq2d 5466 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶))) |
74 | 73 | sseq1d 3632 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢)) |
75 | 69, 74 | anbi12d 747 |
. . . . . . . . . . . 12
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → ((𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ ((int‘𝐾)‘𝑡) ∧ (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢))) |
76 | 75 | rspcev 3309 |
. . . . . . . . . . 11
⊢
((((int‘𝐾)‘𝑡) ∈ 𝐾 ∧ (𝐵 ∈ ((int‘𝐾)‘𝑡) ∧ (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢)) → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
77 | 47, 61, 68, 76 | syl12anc 1324 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
78 | 77 | rexlimdvaa 3032 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
79 | 40, 78 | impbid2 216 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) |
80 | 12, 27, 79 | 3bitr4rd 301 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)) |
81 | 80 | anassrs 680 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) ∧ 𝑥 ∈ 𝑢) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)) |
82 | 81 | pm5.74da 723 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) → ((𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢))) |
83 | 82 | ralbidva 2985 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢))) |
84 | 83 | pm5.32da 673 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)))) |
85 | | limcflf.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
86 | 85, 18, 52, 28 | ellimc2 23641 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) |
87 | 42 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐾 ∈
(TopOn‘ℂ)) |
88 | 85, 18, 51, 28, 15, 13 | limcflflem 23644 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶)) |
89 | | fssres 6070 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶ℂ) |
90 | 85, 17, 89 | sylancl 694 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶ℂ) |
91 | | isflf 21797 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝐿 ∈
(Fil‘𝐶) ∧ (𝐹 ↾ 𝐶):𝐶⟶ℂ) → (𝑥 ∈ ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)))) |
92 | 87, 88, 90, 91 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)))) |
93 | 84, 86, 92 | 3bitr4d 300 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ 𝑥 ∈ ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)))) |
94 | 93 | eqrdv 2620 |
1
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶))) |