Step | Hyp | Ref
| Expression |
1 | | limcrcl 23638 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) → ((𝐹 ↾ 𝐶):dom (𝐹 ↾ 𝐶)⟶ℂ ∧ dom (𝐹 ↾ 𝐶) ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
2 | 1 | simp3d 1075 |
. . . . 5
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) → 𝐵 ∈ ℂ) |
3 | | limccl 23639 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐶) limℂ 𝐵) ⊆ ℂ |
4 | 3 | sseli 3599 |
. . . . 5
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) → 𝑥 ∈ ℂ) |
5 | 2, 4 | jca 554 |
. . . 4
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ))) |
7 | | limcrcl 23638 |
. . . . . 6
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
8 | 7 | simp3d 1075 |
. . . . 5
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝐵 ∈ ℂ) |
9 | | limccl 23639 |
. . . . . 6
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ |
10 | 9 | sseli 3599 |
. . . . 5
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝑥 ∈ ℂ) |
11 | 8, 10 | jca 554 |
. . . 4
⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ))) |
13 | | limcres.j |
. . . . . . . 8
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
14 | | limcres.k |
. . . . . . . . . 10
⊢ 𝐾 =
(TopOpen‘ℂfld) |
15 | 14 | cnfldtopon 22586 |
. . . . . . . . 9
⊢ 𝐾 ∈
(TopOn‘ℂ) |
16 | | limcres.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
17 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐴 ⊆ ℂ) |
18 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐵 ∈ ℂ) |
19 | 18 | snssd 4340 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → {𝐵} ⊆ ℂ) |
20 | 17, 19 | unssd 3789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) ⊆ ℂ) |
21 | | resttopon 20965 |
. . . . . . . . 9
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) →
(𝐾 ↾t
(𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
22 | 15, 20, 21 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
23 | 13, 22 | syl5eqel 2705 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
24 | | topontop 20718 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})) → 𝐽 ∈ Top) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐽 ∈ Top) |
26 | | limcres.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐶 ⊆ 𝐴) |
28 | | unss1 3782 |
. . . . . . . 8
⊢ (𝐶 ⊆ 𝐴 → (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵})) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵})) |
30 | | toponuni 20719 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})) → (𝐴 ∪ {𝐵}) = ∪ 𝐽) |
31 | 23, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) = ∪ 𝐽) |
32 | 29, 31 | sseqtrd 3641 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐶 ∪ {𝐵}) ⊆ ∪
𝐽) |
33 | | limcres.i |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵}))) |
34 | 33 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵}))) |
35 | | elun 3753 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ {𝐵})) |
36 | | simplrr 801 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ ℂ) |
37 | | limcres.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
38 | 37 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐹:𝐴⟶ℂ) |
39 | 38 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
40 | 36, 39 | ifcld 4131 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ 𝐴) → if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧)) ∈ ℂ) |
41 | | elsni 4194 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ {𝐵} → 𝑧 = 𝐵) |
42 | 41 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → 𝑧 = 𝐵) |
43 | 42 | iftrued 4094 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧)) = 𝑥) |
44 | | simplrr 801 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → 𝑥 ∈ ℂ) |
45 | 43, 44 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧)) ∈ ℂ) |
46 | 40, 45 | jaodan 826 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ {𝐵})) → if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧)) ∈ ℂ) |
47 | 35, 46 | sylan2b 492 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ (𝐴 ∪ {𝐵})) → if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧)) ∈ ℂ) |
48 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) |
49 | 47, 48 | fmptd 6385 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))):(𝐴 ∪ {𝐵})⟶ℂ) |
50 | 31 | feq2d 6031 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))):(𝐴 ∪ {𝐵})⟶ℂ ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))):∪ 𝐽⟶ℂ)) |
51 | 49, 50 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))):∪ 𝐽⟶ℂ) |
52 | | eqid 2622 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
53 | 15 | toponunii 20721 |
. . . . . . 7
⊢ ℂ =
∪ 𝐾 |
54 | 52, 53 | cnprest 21093 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝐶 ∪ {𝐵}) ⊆ ∪
𝐽) ∧ (𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})) ∧ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))):∪ 𝐽⟶ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
55 | 25, 32, 34, 51, 54 | syl22anc 1327 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
56 | 13, 14, 48, 38, 17, 18 | ellimc 23637 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (𝐹 limℂ 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵))) |
57 | | eqid 2622 |
. . . . . . 7
⊢ (𝐾 ↾t (𝐶 ∪ {𝐵})) = (𝐾 ↾t (𝐶 ∪ {𝐵})) |
58 | | eqid 2622 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧))) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧))) |
59 | 38, 27 | fssresd 6071 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐹 ↾ 𝐶):𝐶⟶ℂ) |
60 | 27, 17 | sstrd 3613 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐶 ⊆ ℂ) |
61 | 57, 14, 58, 59, 60, 18 | ellimc 23637 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) ↔ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧))) ∈ (((𝐾 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
62 | 29 | resmptd 5452 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ↾ (𝐶 ∪ {𝐵})) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧)))) |
63 | | elun 3753 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↔ (𝑧 ∈ 𝐶 ∨ 𝑧 ∈ {𝐵})) |
64 | | velsn 4193 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵) |
65 | 64 | orbi2i 541 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐶 ∨ 𝑧 ∈ {𝐵}) ↔ (𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵)) |
66 | 63, 65 | bitri 264 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↔ (𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵)) |
67 | | pm5.61 749 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) ↔ (𝑧 ∈ 𝐶 ∧ ¬ 𝑧 = 𝐵)) |
68 | | fvres 6207 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑧) = (𝐹‘𝑧)) |
69 | 68 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐶 ∧ ¬ 𝑧 = 𝐵) → ((𝐹 ↾ 𝐶)‘𝑧) = (𝐹‘𝑧)) |
70 | 67, 69 | sylbi 207 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) → ((𝐹 ↾ 𝐶)‘𝑧) = (𝐹‘𝑧)) |
71 | 70 | ifeq2da 4117 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∨ 𝑧 = 𝐵) → if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧)) = if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) |
72 | 66, 71 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐶 ∪ {𝐵}) → if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧)) = if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) |
73 | 72 | mpteq2ia 4740 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧))) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) |
74 | 62, 73 | syl6reqr 2675 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧))) = ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ↾ (𝐶 ∪ {𝐵}))) |
75 | 13 | oveq1i 6660 |
. . . . . . . . . 10
⊢ (𝐽 ↾t (𝐶 ∪ {𝐵})) = ((𝐾 ↾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) |
76 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐾 ∈
(TopOn‘ℂ)) |
77 | | cnex 10017 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
78 | 77 | ssex 4802 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∪ {𝐵}) ⊆ ℂ → (𝐴 ∪ {𝐵}) ∈ V) |
79 | 20, 78 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) ∈ V) |
80 | | restabs 20969 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}) ∧ (𝐴 ∪ {𝐵}) ∈ V) → ((𝐾 ↾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) = (𝐾 ↾t (𝐶 ∪ {𝐵}))) |
81 | 76, 29, 79, 80 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝐾 ↾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) = (𝐾 ↾t (𝐶 ∪ {𝐵}))) |
82 | 75, 81 | syl5req 2669 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐾 ↾t (𝐶 ∪ {𝐵})) = (𝐽 ↾t (𝐶 ∪ {𝐵}))) |
83 | 82 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝐾 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾) = ((𝐽 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)) |
84 | 83 | fveq1d 6193 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (((𝐾 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵) = (((𝐽 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
85 | 74, 84 | eleq12d 2695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹 ↾ 𝐶)‘𝑧))) ∈ (((𝐾 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
86 | 61, 85 | bitrd 268 |
. . . . 5
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹‘𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽 ↾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
87 | 55, 56, 86 | 3bitr4rd 301 |
. . . 4
⊢ ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) ↔ 𝑥 ∈ (𝐹 limℂ 𝐵))) |
88 | 87 | ex 450 |
. . 3
⊢ (𝜑 → ((𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) ↔ 𝑥 ∈ (𝐹 limℂ 𝐵)))) |
89 | 6, 12, 88 | pm5.21ndd 369 |
. 2
⊢ (𝜑 → (𝑥 ∈ ((𝐹 ↾ 𝐶) limℂ 𝐵) ↔ 𝑥 ∈ (𝐹 limℂ 𝐵))) |
90 | 89 | eqrdv 2620 |
1
⊢ (𝜑 → ((𝐹 ↾ 𝐶) limℂ 𝐵) = (𝐹 limℂ 𝐵)) |