Step | Hyp | Ref
| Expression |
1 | | limcresioolb.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
2 | | limcresioolb.cled |
. . . . . 6
⊢ (𝜑 → 𝐶 ≤ 𝐷) |
3 | | iooss2 13114 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ*
∧ 𝐶 ≤ 𝐷) → (𝐵(,)𝐶) ⊆ (𝐵(,)𝐷)) |
4 | 1, 2, 3 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐵(,)𝐷)) |
5 | 4 | resabs1d 5921 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)) = (𝐹 ↾ (𝐵(,)𝐶))) |
6 | 5 | eqcomd 2746 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐶)) = ((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶))) |
7 | 6 | oveq1d 7286 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = (((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)) limℂ 𝐵)) |
8 | | limcresioolb.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
9 | | fresin 6641 |
. . . 4
⊢ (𝐹:𝐴⟶ℂ → (𝐹 ↾ (𝐵(,)𝐷)):(𝐴 ∩ (𝐵(,)𝐷))⟶ℂ) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵(,)𝐷)):(𝐴 ∩ (𝐵(,)𝐷))⟶ℂ) |
11 | | limcresioolb.bcss |
. . . 4
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ 𝐴) |
12 | 11, 4 | ssind 4172 |
. . 3
⊢ (𝜑 → (𝐵(,)𝐶) ⊆ (𝐴 ∩ (𝐵(,)𝐷))) |
13 | | inss2 4169 |
. . . . 5
⊢ (𝐴 ∩ (𝐵(,)𝐷)) ⊆ (𝐵(,)𝐷) |
14 | | ioosscn 13140 |
. . . . 5
⊢ (𝐵(,)𝐷) ⊆ ℂ |
15 | 13, 14 | sstri 3935 |
. . . 4
⊢ (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℂ |
16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℂ) |
17 | | eqid 2740 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
18 | | eqid 2740 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
19 | | limcresioolb.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
20 | 19 | rexrd 11026 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
21 | | limcresioolb.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
22 | | limcresioolb.bltc |
. . . . 5
⊢ (𝜑 → 𝐵 < 𝐶) |
23 | | lbico1 13132 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → 𝐵 ∈ (𝐵[,)𝐶)) |
24 | 20, 21, 22, 23 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (𝐵[,)𝐶)) |
25 | | snunioo1 43021 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝐵
< 𝐶) → ((𝐵(,)𝐶) ∪ {𝐵}) = (𝐵[,)𝐶)) |
26 | 20, 21, 22, 25 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 → ((𝐵(,)𝐶) ∪ {𝐵}) = (𝐵[,)𝐶)) |
27 | 26 | fveq2d 6775 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘((𝐵(,)𝐶) ∪ {𝐵})) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘(𝐵[,)𝐶))) |
28 | 17 | cnfldtop 23945 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
29 | | ovex 7304 |
. . . . . . . . . 10
⊢ (𝐵(,)𝐷) ∈ V |
30 | 29 | inex2 5246 |
. . . . . . . . 9
⊢ (𝐴 ∩ (𝐵(,)𝐷)) ∈ V |
31 | | snex 5358 |
. . . . . . . . 9
⊢ {𝐵} ∈ V |
32 | 30, 31 | unex 7590 |
. . . . . . . 8
⊢ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V |
33 | | resttop 22309 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V) →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top) |
34 | 28, 32, 33 | mp2an 689 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top) |
36 | | mnfxr 11033 |
. . . . . . . . . . . . 13
⊢ -∞
∈ ℝ* |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → -∞ ∈
ℝ*) |
38 | 21 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐶 ∈
ℝ*) |
39 | | icossre 13159 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ*)
→ (𝐵[,)𝐶) ⊆
ℝ) |
40 | 19, 21, 39 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵[,)𝐶) ⊆ ℝ) |
41 | 40 | sselda 3926 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ ℝ) |
42 | 41 | mnfltd 12859 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → -∞ < 𝑥) |
43 | 20 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐵 ∈
ℝ*) |
44 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ (𝐵[,)𝐶)) |
45 | | icoltub 43017 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,)𝐶)) → 𝑥 < 𝐶) |
46 | 43, 38, 44, 45 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 < 𝐶) |
47 | 37, 38, 41, 42, 46 | eliood 43007 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ (-∞(,)𝐶)) |
48 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝐵) |
49 | | snidg 4601 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → 𝐵 ∈ {𝐵}) |
50 | | elun2 4116 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
51 | 19, 49, 50 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐵 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
53 | 48, 52 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
54 | 53 | adantlr 712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
55 | | simpll 764 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝜑) |
56 | 43 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈
ℝ*) |
57 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐶 ∈
ℝ*) |
58 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ) |
59 | 19 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈ ℝ) |
60 | | icogelb 13129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,)𝐶)) → 𝐵 ≤ 𝑥) |
61 | 43, 38, 44, 60 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝐵 ≤ 𝑥) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ≤ 𝑥) |
63 | | neqne 2953 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 = 𝐵 → 𝑥 ≠ 𝐵) |
64 | 63 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ≠ 𝐵) |
65 | 59, 58, 62, 64 | leneltd 11129 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝐵 < 𝑥) |
66 | 46 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐶) |
67 | 56, 57, 58, 65, 66 | eliood 43007 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐶)) |
68 | 12 | sselda 3926 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷))) |
69 | | elun1 4115 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷)) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵(,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
71 | 55, 67, 70 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
72 | 54, 71 | pm2.61dan 810 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
73 | 47, 72 | elind 4133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵[,)𝐶)) → 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
74 | 24 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐵 ∈ (𝐵[,)𝐶)) |
75 | 48, 74 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,)𝐶)) |
76 | 75 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,)𝐶)) |
77 | | ioossico 13169 |
. . . . . . . . . . . 12
⊢ (𝐵(,)𝐶) ⊆ (𝐵[,)𝐶) |
78 | 20 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈
ℝ*) |
79 | 21 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐶 ∈
ℝ*) |
80 | | elinel1 4134 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) → 𝑥 ∈ (-∞(,)𝐶)) |
81 | 80 | elioored 43058 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) → 𝑥 ∈ ℝ) |
82 | 81 | ad2antlr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ℝ) |
83 | 1 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐷 ∈
ℝ*) |
84 | | elinel2 4135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) → 𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
85 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 = 𝐵 → ¬ 𝑥 = 𝐵) |
86 | | velsn 4583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵) |
87 | 85, 86 | sylnibr 329 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 = 𝐵 → ¬ 𝑥 ∈ {𝐵}) |
88 | | elunnel2 42552 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∧ ¬ 𝑥 ∈ {𝐵}) → 𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷))) |
89 | 84, 87, 88 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴 ∩ (𝐵(,)𝐷))) |
90 | 13, 89 | sselid 3924 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐷)) |
91 | 90 | adantll 711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐷)) |
92 | | ioogtlb 43004 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝐷 ∈
ℝ* ∧ 𝑥
∈ (𝐵(,)𝐷)) → 𝐵 < 𝑥) |
93 | 78, 83, 91, 92 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝐵 < 𝑥) |
94 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → -∞ ∈
ℝ*) |
95 | 21 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝐶 ∈
ℝ*) |
96 | 80 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝑥 ∈ (-∞(,)𝐶)) |
97 | | iooltub 43019 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝐶)) → 𝑥 < 𝐶) |
98 | 94, 95, 96, 97 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝑥 < 𝐶) |
99 | 98 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 < 𝐶) |
100 | 78, 79, 82, 93, 99 | eliood 43007 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵(,)𝐶)) |
101 | 77, 100 | sselid 3924 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐵[,)𝐶)) |
102 | 76, 101 | pm2.61dan 810 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) → 𝑥 ∈ (𝐵[,)𝐶)) |
103 | 73, 102 | impbida 798 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐵[,)𝐶) ↔ 𝑥 ∈ ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))) |
104 | 103 | eqrdv 2738 |
. . . . . . . 8
⊢ (𝜑 → (𝐵[,)𝐶) = ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
105 | | retop 23923 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) ∈ Top |
106 | 105 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
107 | 32 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V) |
108 | | iooretop 23927 |
. . . . . . . . . 10
⊢
(-∞(,)𝐶)
∈ (topGen‘ran (,)) |
109 | 108 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (-∞(,)𝐶) ∈ (topGen‘ran
(,))) |
110 | | elrestr 17137 |
. . . . . . . . 9
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ∈ V ∧ (-∞(,)𝐶) ∈ (topGen‘ran (,)))
→ ((-∞(,)𝐶)
∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
111 | 106, 107,
109, 110 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → ((-∞(,)𝐶) ∩ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
112 | 104, 111 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (𝐵[,)𝐶) ∈ ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
113 | 17 | tgioo2 23964 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
114 | 113 | oveq1i 7281 |
. . . . . . . 8
⊢
((topGen‘ran (,)) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) =
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵})) |
115 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
116 | | ioossre 13139 |
. . . . . . . . . . . 12
⊢ (𝐵(,)𝐷) ⊆ ℝ |
117 | 13, 116 | sstri 3935 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℝ |
118 | 117 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ (𝐵(,)𝐷)) ⊆ ℝ) |
119 | 19 | snssd 4748 |
. . . . . . . . . 10
⊢ (𝜑 → {𝐵} ⊆ ℝ) |
120 | 118, 119 | unssd 4125 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ⊆ ℝ) |
121 | | reex 10963 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
122 | 121 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
V) |
123 | | restabs 22314 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
124 | 115, 120,
122, 123 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
125 | 114, 124 | eqtrid 2792 |
. . . . . . 7
⊢ (𝜑 → ((topGen‘ran (,))
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵})) = ((TopOpen‘ℂfld)
↾t ((𝐴
∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
126 | 112, 125 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → (𝐵[,)𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) |
127 | | isopn3i 22231 |
. . . . . 6
⊢
((((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})) ∈ Top ∧ (𝐵[,)𝐶) ∈
((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵}))) →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘(𝐵[,)𝐶)) = (𝐵[,)𝐶)) |
128 | 35, 126, 127 | syl2anc 584 |
. . . . 5
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘(𝐵[,)𝐶)) = (𝐵[,)𝐶)) |
129 | 27, 128 | eqtr2d 2781 |
. . . 4
⊢ (𝜑 → (𝐵[,)𝐶) =
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘((𝐵(,)𝐶) ∪ {𝐵}))) |
130 | 24, 129 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝐵 ∈
((int‘((TopOpen‘ℂfld) ↾t ((𝐴 ∩ (𝐵(,)𝐷)) ∪ {𝐵})))‘((𝐵(,)𝐶) ∪ {𝐵}))) |
131 | 10, 12, 16, 17, 18, 130 | limcres 25048 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (𝐵(,)𝐷)) ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵)) |
132 | 7, 131 | eqtrd 2780 |
1
⊢ (𝜑 → ((𝐹 ↾ (𝐵(,)𝐶)) limℂ 𝐵) = ((𝐹 ↾ (𝐵(,)𝐷)) limℂ 𝐵)) |