| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑡 ∈ V | 
| 2 | 1 | inex1 5317 | . . . . . . . . . 10
⊢ (𝑡 ∩ 𝐶) ∈ V | 
| 3 | 2 | rgenw 3065 | . . . . . . . . 9
⊢
∀𝑡 ∈
((nei‘𝐾)‘{𝐵})(𝑡 ∩ 𝐶) ∈ V | 
| 4 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶)) = (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶)) | 
| 5 |  | imaeq2 6074 | . . . . . . . . . . . 12
⊢ (𝑠 = (𝑡 ∩ 𝐶) → ((𝐹 ↾ 𝐶) “ 𝑠) = ((𝐹 ↾ 𝐶) “ (𝑡 ∩ 𝐶))) | 
| 6 |  | inss2 4238 | . . . . . . . . . . . . 13
⊢ (𝑡 ∩ 𝐶) ⊆ 𝐶 | 
| 7 |  | resima2 6034 | . . . . . . . . . . . . 13
⊢ ((𝑡 ∩ 𝐶) ⊆ 𝐶 → ((𝐹 ↾ 𝐶) “ (𝑡 ∩ 𝐶)) = (𝐹 “ (𝑡 ∩ 𝐶))) | 
| 8 | 6, 7 | ax-mp 5 | . . . . . . . . . . . 12
⊢ ((𝐹 ↾ 𝐶) “ (𝑡 ∩ 𝐶)) = (𝐹 “ (𝑡 ∩ 𝐶)) | 
| 9 | 5, 8 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (𝑠 = (𝑡 ∩ 𝐶) → ((𝐹 ↾ 𝐶) “ 𝑠) = (𝐹 “ (𝑡 ∩ 𝐶))) | 
| 10 | 9 | sseq1d 4015 | . . . . . . . . . 10
⊢ (𝑠 = (𝑡 ∩ 𝐶) → (((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) | 
| 11 | 4, 10 | rexrnmptw 7115 | . . . . . . . . 9
⊢
(∀𝑡 ∈
((nei‘𝐾)‘{𝐵})(𝑡 ∩ 𝐶) ∈ V → (∃𝑠 ∈ ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) | 
| 12 | 3, 11 | mp1i 13 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑠 ∈ ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) | 
| 13 |  | limcflf.l | . . . . . . . . . 10
⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) | 
| 14 |  | fvex 6919 | . . . . . . . . . . 11
⊢
((nei‘𝐾)‘{𝐵}) ∈ V | 
| 15 |  | limcflf.c | . . . . . . . . . . . . . . 15
⊢ 𝐶 = (𝐴 ∖ {𝐵}) | 
| 16 |  | difss 4136 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 | 
| 17 | 15, 16 | eqsstri 4030 | . . . . . . . . . . . . . 14
⊢ 𝐶 ⊆ 𝐴 | 
| 18 |  | limcflf.a | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 19 | 17, 18 | sstrid 3995 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ⊆ ℂ) | 
| 20 |  | cnex 11236 | . . . . . . . . . . . . . 14
⊢ ℂ
∈ V | 
| 21 | 20 | ssex 5321 | . . . . . . . . . . . . 13
⊢ (𝐶 ⊆ ℂ → 𝐶 ∈ V) | 
| 22 | 19, 21 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ V) | 
| 23 | 22 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → 𝐶 ∈ V) | 
| 24 |  | restval 17471 | . . . . . . . . . . 11
⊢
((((nei‘𝐾)‘{𝐵}) ∈ V ∧ 𝐶 ∈ V) → (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) = ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))) | 
| 25 | 14, 23, 24 | sylancr 587 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (((nei‘𝐾)‘{𝐵}) ↾t 𝐶) = ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))) | 
| 26 | 13, 25 | eqtrid 2789 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → 𝐿 = ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))) | 
| 27 | 26 | rexeqdv 3327 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢 ↔ ∃𝑠 ∈ ran (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↦ (𝑡 ∩ 𝐶))((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)) | 
| 28 |  | limcflf.k | . . . . . . . . . . . . . 14
⊢ 𝐾 =
(TopOpen‘ℂfld) | 
| 29 | 28 | cnfldtop 24804 | . . . . . . . . . . . . 13
⊢ 𝐾 ∈ Top | 
| 30 |  | opnneip 23127 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤) → 𝑤 ∈ ((nei‘𝐾)‘{𝐵})) | 
| 31 | 29, 30 | mp3an1 1450 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤) → 𝑤 ∈ ((nei‘𝐾)‘{𝐵})) | 
| 32 |  | id 22 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤) | 
| 33 | 15 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑤 → 𝐶 = (𝐴 ∖ {𝐵})) | 
| 34 | 32, 33 | ineq12d 4221 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑤 → (𝑡 ∩ 𝐶) = (𝑤 ∩ (𝐴 ∖ {𝐵}))) | 
| 35 | 34 | imaeq2d 6078 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑤 → (𝐹 “ (𝑡 ∩ 𝐶)) = (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵})))) | 
| 36 | 35 | sseq1d 4015 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑤 → ((𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢 ↔ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) | 
| 37 | 36 | rspcev 3622 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) | 
| 38 | 31, 37 | sylan 580 | . . . . . . . . . . 11
⊢ (((𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤) ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) | 
| 39 | 38 | anasss 466 | . . . . . . . . . 10
⊢ ((𝑤 ∈ 𝐾 ∧ (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) | 
| 40 | 39 | rexlimiva 3147 | . . . . . . . . 9
⊢
(∃𝑤 ∈
𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) → ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) | 
| 41 |  | simprl 771 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝑡 ∈ ((nei‘𝐾)‘{𝐵})) | 
| 42 | 28 | cnfldtopon 24803 | . . . . . . . . . . . . . . 15
⊢ 𝐾 ∈
(TopOn‘ℂ) | 
| 43 | 42 | toponunii 22922 | . . . . . . . . . . . . . 14
⊢ ℂ =
∪ 𝐾 | 
| 44 | 43 | neii1 23114 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝑡 ∈ ((nei‘𝐾)‘{𝐵})) → 𝑡 ⊆ ℂ) | 
| 45 | 29, 41, 44 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝑡 ⊆ ℂ) | 
| 46 | 43 | ntropn 23057 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ Top ∧ 𝑡 ⊆ ℂ) →
((int‘𝐾)‘𝑡) ∈ 𝐾) | 
| 47 | 29, 45, 46 | sylancr 587 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → ((int‘𝐾)‘𝑡) ∈ 𝐾) | 
| 48 | 43 | lpss 23150 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Top ∧ 𝐴 ⊆ ℂ) →
((limPt‘𝐾)‘𝐴) ⊆ ℂ) | 
| 49 | 29, 18, 48 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((limPt‘𝐾)‘𝐴) ⊆ ℂ) | 
| 50 |  | limcflf.b | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴)) | 
| 51 | 49, 50 | sseldd 3984 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 52 | 51 | snssd 4809 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝐵} ⊆ ℂ) | 
| 53 | 52 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → {𝐵} ⊆ ℂ) | 
| 54 | 43 | neiint 23112 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ {𝐵} ⊆ ℂ ∧ 𝑡 ⊆ ℂ) → (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) | 
| 55 | 29, 53, 45, 54 | mp3an2i 1468 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) | 
| 56 | 41, 55 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → {𝐵} ⊆ ((int‘𝐾)‘𝑡)) | 
| 57 | 51 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝐵 ∈ ℂ) | 
| 58 |  | snssg 4783 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℂ → (𝐵 ∈ ((int‘𝐾)‘𝑡) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐵 ∈ ((int‘𝐾)‘𝑡) ↔ {𝐵} ⊆ ((int‘𝐾)‘𝑡))) | 
| 60 | 56, 59 | mpbird 257 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → 𝐵 ∈ ((int‘𝐾)‘𝑡)) | 
| 61 | 43 | ntrss2 23065 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ Top ∧ 𝑡 ⊆ ℂ) →
((int‘𝐾)‘𝑡) ⊆ 𝑡) | 
| 62 | 29, 45, 61 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → ((int‘𝐾)‘𝑡) ⊆ 𝑡) | 
| 63 |  | ssrin 4242 | . . . . . . . . . . . . 13
⊢
(((int‘𝐾)‘𝑡) ⊆ 𝑡 → (((int‘𝐾)‘𝑡) ∩ 𝐶) ⊆ (𝑡 ∩ 𝐶)) | 
| 64 |  | imass2 6120 | . . . . . . . . . . . . 13
⊢
((((int‘𝐾)‘𝑡) ∩ 𝐶) ⊆ (𝑡 ∩ 𝐶) → (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ (𝐹 “ (𝑡 ∩ 𝐶))) | 
| 65 | 62, 63, 64 | 3syl 18 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ (𝐹 “ (𝑡 ∩ 𝐶))) | 
| 66 |  | simprr 773 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢) | 
| 67 | 65, 66 | sstrd 3994 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢) | 
| 68 |  | eleq2 2830 | . . . . . . . . . . . . 13
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝐵 ∈ 𝑤 ↔ 𝐵 ∈ ((int‘𝐾)‘𝑡))) | 
| 69 | 15 | ineq2i 4217 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∩ 𝐶) = (𝑤 ∩ (𝐴 ∖ {𝐵})) | 
| 70 |  | ineq1 4213 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝑤 ∩ 𝐶) = (((int‘𝐾)‘𝑡) ∩ 𝐶)) | 
| 71 | 69, 70 | eqtr3id 2791 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝑤 ∩ (𝐴 ∖ {𝐵})) = (((int‘𝐾)‘𝑡) ∩ 𝐶)) | 
| 72 | 71 | imaeq2d 6078 | . . . . . . . . . . . . . 14
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶))) | 
| 73 | 72 | sseq1d 4015 | . . . . . . . . . . . . 13
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢)) | 
| 74 | 68, 73 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑤 = ((int‘𝐾)‘𝑡) → ((𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ ((int‘𝐾)‘𝑡) ∧ (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢))) | 
| 75 | 74 | rspcev 3622 | . . . . . . . . . . 11
⊢
((((int‘𝐾)‘𝑡) ∈ 𝐾 ∧ (𝐵 ∈ ((int‘𝐾)‘𝑡) ∧ (𝐹 “ (((int‘𝐾)‘𝑡) ∩ 𝐶)) ⊆ 𝑢)) → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) | 
| 76 | 47, 60, 67, 75 | syl12anc 837 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) ∧ (𝑡 ∈ ((nei‘𝐾)‘{𝐵}) ∧ (𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) | 
| 77 | 76 | rexlimdvaa 3156 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) | 
| 78 | 40, 77 | impbid2 226 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑡 ∈ ((nei‘𝐾)‘{𝐵})(𝐹 “ (𝑡 ∩ 𝐶)) ⊆ 𝑢)) | 
| 79 | 12, 27, 78 | 3bitr4rd 312 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢)) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)) | 
| 80 | 79 | anassrs 467 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) ∧ 𝑥 ∈ 𝑢) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)) | 
| 81 | 80 | pm5.74da 804 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) → ((𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢))) | 
| 82 | 81 | ralbidva 3176 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢))) | 
| 83 | 82 | pm5.32da 579 | . . 3
⊢ (𝜑 → ((𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)))) | 
| 84 |  | limcflf.f | . . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 85 | 84, 18, 51, 28 | ellimc2 25912 | . . 3
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) | 
| 86 | 84, 18, 50, 28, 15, 13 | limcflflem 25915 | . . . 4
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶)) | 
| 87 |  | fssres 6774 | . . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶ℂ) | 
| 88 | 84, 17, 87 | sylancl 586 | . . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶ℂ) | 
| 89 |  | isflf 24001 | . . . 4
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝐿 ∈
(Fil‘𝐶) ∧ (𝐹 ↾ 𝐶):𝐶⟶ℂ) → (𝑥 ∈ ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)))) | 
| 90 | 42, 86, 88, 89 | mp3an2i 1468 | . . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝑥 ∈ 𝑢 → ∃𝑠 ∈ 𝐿 ((𝐹 ↾ 𝐶) “ 𝑠) ⊆ 𝑢)))) | 
| 91 | 83, 85, 90 | 3bitr4d 311 | . 2
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ 𝑥 ∈ ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)))) | 
| 92 | 91 | eqrdv 2735 | 1
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶))) |