Step | Hyp | Ref
| Expression |
1 | | cncfiooicclem1.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | limccl 23445 |
. . . . . . 7
⊢ (𝐹 limℂ 𝐴) ⊆
ℂ |
3 | | cncfiooicclem1.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) |
4 | 2, 3 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℂ) |
5 | 4 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → 𝑅 ∈ ℂ) |
6 | | limccl 23445 |
. . . . . . . 8
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ |
7 | | cncfiooicclem1.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) |
8 | 6, 7 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℂ) |
9 | 8 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ) |
10 | | simplll 794 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝜑) |
11 | | orel1 396 |
. . . . . . . . . . 11
⊢ (¬
𝑥 = 𝐴 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑥 = 𝐵)) |
12 | 11 | con3dimp 456 |
. . . . . . . . . 10
⊢ ((¬
𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
13 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
14 | 13 | elpr 4146 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) |
15 | 12, 14 | sylnibr 318 |
. . . . . . . . 9
⊢ ((¬
𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵}) |
16 | 15 | adantll 746 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵}) |
17 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵)) |
18 | | cncfiooicclem1.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
19 | 18 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
20 | 10, 19 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈
ℝ*) |
21 | | cncfiooicclem1.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℝ) |
22 | 21 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
23 | 10, 22 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈
ℝ*) |
24 | | cncfiooicclem1.altb |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝐵) |
25 | 18, 21, 24 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
26 | 10, 25 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ≤ 𝐵) |
27 | | prunioo 12172 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |
28 | 20, 23, 26, 27 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |
29 | 17, 28 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) |
30 | | elun 3715 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵})) |
31 | 29, 30 | sylib 207 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵})) |
32 | | orel2 397 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ {𝐴, 𝐵} → ((𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}) → 𝑥 ∈ (𝐴(,)𝐵))) |
33 | 16, 31, 32 | sylc 63 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵)) |
34 | | cncfiooicclem1.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
35 | | cncff 22504 |
. . . . . . . . 9
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) |
37 | 36 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
38 | 10, 33, 37 | syl2anc 691 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) ∈ ℂ) |
39 | 9, 38 | ifclda 4070 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) ∈ ℂ) |
40 | 5, 39 | ifclda 4070 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) |
41 | | cncfiooicclem1.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
42 | 1, 40, 41 | fmptdf 6294 |
. . 3
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
43 | | elun 3715 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) |
44 | 19, 22, 25, 27 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) |
45 | 44 | eleq2d 2673 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵))) |
46 | 43, 45 | syl5bbr 273 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵))) |
47 | 46 | biimpar 501 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) |
48 | | ioossicc 12130 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
49 | | fssres 5983 |
. . . . . . . . . . . . 13
⊢ ((𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ) |
50 | 42, 48, 49 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ) |
51 | 50 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦))) |
52 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
53 | 41, 52 | nfcxfr 2749 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐺 |
54 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝐴(,)𝐵) |
55 | 53, 54 | nfres 5319 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝐺 ↾ (𝐴(,)𝐵)) |
56 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑦 |
57 | 55, 56 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) |
58 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝐺 ↾ (𝐴(,)𝐵)) |
59 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝑥 |
60 | 58, 59 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) |
61 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) = ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) |
62 | 57, 60, 61 | cbvmpt 4677 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) |
63 | 62 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))) |
64 | | fvres 6117 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺‘𝑥)) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺‘𝑥)) |
66 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
67 | 48, 66 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) |
68 | 4 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ) |
69 | 8 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ) |
70 | 37 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) ∈ ℂ) |
71 | 69, 70 | ifclda 4070 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) ∈ ℂ) |
72 | 68, 71 | ifcld 4081 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) |
73 | 41 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
74 | 67, 72, 73 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) |
75 | | elioo4g 12105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑥 ∈ ℝ)
∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
76 | 75 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑥 ∈ ℝ)
∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
77 | 76 | simpld 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑥 ∈
ℝ)) |
78 | 77 | simp1d 1066 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 ∈
ℝ*) |
79 | | elioore 12076 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) |
80 | 79 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*) |
81 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
82 | 81 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑥) |
83 | | xrltne 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝐴
< 𝑥) → 𝑥 ≠ 𝐴) |
84 | 78, 80, 82, 83 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ≠ 𝐴) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 𝐴) |
86 | 85 | neneqd 2787 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴) |
87 | 86 | iffalsed 4047 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) |
88 | 81 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 < 𝐵) |
89 | 79, 88 | ltned 10052 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ≠ 𝐵) |
90 | 89 | neneqd 2787 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵) |
91 | 90 | iffalsed 4047 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴(,)𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥)) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥)) |
93 | 87, 92 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = (𝐹‘𝑥)) |
94 | 65, 74, 93 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥)) |
95 | 1, 94 | mpteq2da 4671 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
96 | 51, 63, 95 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
97 | 36 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) |
98 | | ioosscn 38563 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℂ |
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
100 | | ssid 3587 |
. . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ |
101 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
102 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) |
103 | 101 | cnfldtop 22397 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈ Top |
104 | | unicntop 38230 |
. . . . . . . . . . . . . . . 16
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
105 | 104 | restid 15917 |
. . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
106 | 103, 105 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
107 | 106 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
108 | 101, 102,
107 | cncfcn 22520 |
. . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
109 | 99, 100, 108 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
110 | 34, 97, 109 | 3eltr3d 2702 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
111 | 96, 110 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) |
112 | 104 | restuni 20776 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ ℂ) → (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) |
113 | 103, 98, 112 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) |
114 | 113 | cncnpi 20892 |
. . . . . . . . 9
⊢ (((𝐺 ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
115 | 111, 114 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
116 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
(TopOpen‘ℂfld) ∈ Top) |
117 | 48 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
118 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝐴[,]𝐵) ∈ V |
119 | 118 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ∈ V) |
120 | | restabs 20779 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ∈ V) →
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) |
121 | 116, 117,
119, 120 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) |
122 | 121 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵))) |
123 | 122 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) =
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))) |
124 | 123 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = (((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
125 | 115, 124 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
126 | | resttop 20774 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ∈ V) →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top) |
127 | 103, 118,
126 | mp2an 704 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top |
128 | 127 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top) |
129 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
130 | 18, 21 | iccssred 38574 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
131 | | ax-resscn 9872 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
132 | 130, 131 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
133 | 104 | restuni 20776 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐴[,]𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) |
134 | 103, 132,
133 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) |
135 | 129, 134 | sseqtrd 3604 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) |
136 | 135 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) |
137 | | retop 22375 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
138 | 137 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (topGen‘ran (,)) ∈
Top) |
139 | | ioossre 12106 |
. . . . . . . . . . . . . . 15
⊢ (𝐴(,)𝐵) ⊆ ℝ |
140 | | difss 3699 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
∖ (𝐴[,]𝐵)) ⊆
ℝ |
141 | 139, 140 | unssi 3750 |
. . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ |
142 | 141 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ) |
143 | | ssun1 3738 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) |
145 | | uniretop 22376 |
. . . . . . . . . . . . . 14
⊢ ℝ =
∪ (topGen‘ran (,)) |
146 | 145 | ntrss 20669 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵)) ⊆
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
147 | 138, 142,
144, 146 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵)) ⊆
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
148 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴(,)𝐵)) |
149 | | ioontr 38583 |
. . . . . . . . . . . . 13
⊢
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵) |
150 | 148, 149 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵))) |
151 | 147, 150 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) |
152 | 48, 148 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴[,]𝐵)) |
153 | 151, 152 | elind 3760 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
154 | 130 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ) |
155 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) |
156 | 145, 155 | restntr 20796 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
157 | 138, 154,
117, 156 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) |
158 | 153, 157 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((topGen‘ran (,))
↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵))) |
159 | 101 | tgioo2 22414 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (topGen‘ran (,)) =
((TopOpen‘ℂfld) ↾t
ℝ)) |
161 | 160 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) = (((TopOpen‘ℂfld)
↾t ℝ) ↾t (𝐴[,]𝐵))) |
162 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
163 | | reex 9906 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ∈
V) |
165 | | restabs 20779 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) |
166 | 162, 130,
164, 165 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) |
167 | 161, 166 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) |
168 | 167 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 →
(int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) =
(int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))) |
169 | 168 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) =
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵))) |
170 | 169 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) =
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵))) |
171 | 158, 170 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵))) |
172 | 134 | feq2d 5944 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺:(𝐴[,]𝐵)⟶ℂ ↔ 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)) |
173 | 42, 172 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ) |
174 | 173 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ) |
175 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) = ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) |
176 | 175, 104 | cnprest 20903 |
. . . . . . . 8
⊢
(((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top ∧ (𝐴(,)𝐵) ⊆ ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) ∧ (𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) ∧ 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
177 | 128, 136,
171, 174, 176 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) |
178 | 125, 177 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
179 | | elpri 4145 |
. . . . . . 7
⊢ (𝑦 ∈ {𝐴, 𝐵} → (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) |
180 | | lbicc2 12159 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
181 | 19, 22, 25, 180 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
182 | | iftrue 4042 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) |
183 | 182, 41 | fvmptg 6189 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝑅 ∈ (𝐹 limℂ 𝐴)) → (𝐺‘𝐴) = 𝑅) |
184 | 181, 3, 183 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘𝐴) = 𝑅) |
185 | 97 | eqcomd 2616 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) = 𝐹) |
186 | 96, 185 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝐺 ↾ (𝐴(,)𝐵))) |
187 | 186 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 limℂ 𝐴) = ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐴)) |
188 | 3, 187 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐴)) |
189 | 18, 21, 24, 42 | limciccioolb 38688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐴) = (𝐺 limℂ 𝐴)) |
190 | 188, 189 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ (𝐺 limℂ 𝐴)) |
191 | 184, 190 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝐴) ∈ (𝐺 limℂ 𝐴)) |
192 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) |
193 | 101, 192 | cnplimc 23457 |
. . . . . . . . . . . 12
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐴) ∈ (𝐺 limℂ 𝐴)))) |
194 | 132, 181,
193 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐴) ∈ (𝐺 limℂ 𝐴)))) |
195 | 42, 191, 194 | mpbir2and 959 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴)) |
196 | 195 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴)) |
197 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴)) |
198 | 197 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
199 | 198 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐴) →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
200 | 196, 199 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
201 | 21 | leidd 10473 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
202 | 18, 21, 21, 25, 201 | eliccd 38573 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
203 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 = 𝐵 |
204 | 203 | iftruei 4043 |
. . . . . . . . . . . . . . . . 17
⊢ if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)) = 𝐿 |
205 | 204, 8 | syl5eqel 2692 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)) ∈ ℂ) |
206 | 4, 205 | ifcld 4081 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ) |
207 | 202, 206 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ)) |
208 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ) |
209 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝐵 |
210 | 53, 209 | nffv 6110 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝐺‘𝐵) |
211 | 210 | nfeq1 2764 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) |
212 | 208, 211 | nfim 1813 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ) → (𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
213 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝐵 ∈ (𝐴[,]𝐵))) |
214 | 182 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) |
215 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐴) |
216 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 = 𝐴 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) = 𝑅) |
217 | 216 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 = 𝐴 → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
218 | 215, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
219 | 214, 218 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
220 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) |
221 | 220 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) |
222 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = 𝐿) |
223 | 222 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = 𝐿) |
224 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ≠ 𝐴 ↔ ¬ 𝑥 = 𝐴) |
225 | | pm13.18 2863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝐵 ≠ 𝐴) |
226 | 224, 225 | sylan2br 492 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐵 ≠ 𝐴) |
227 | 226 | neneqd 2787 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → ¬ 𝐵 = 𝐴) |
228 | 227 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) |
229 | 228, 204 | syl6req 2661 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐿 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
230 | 221, 223,
229 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
231 | 219, 230 | pm2.61dan 828 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
232 | 231 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → (if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ ↔ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ)) |
233 | 213, 232 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ))) |
234 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → (𝐺‘𝑥) = (𝐺‘𝐵)) |
235 | 234, 231 | eqeq12d 2625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐵 → ((𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ↔ (𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))))) |
236 | 233, 235 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐵 → (((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) ↔ ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ) → (𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))))) |
237 | 212, 236,
73 | vtoclg1f 3238 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝐵 ∈ (𝐴[,]𝐵) ∧ if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ) → (𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))))) |
238 | 202, 207,
237 | sylc 63 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) |
239 | 18, 24 | gtned 10051 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
240 | 239 | neneqd 2787 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐵 = 𝐴) |
241 | 240 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) |
242 | 204 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)) = 𝐿) |
243 | 238, 241,
242 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘𝐵) = 𝐿) |
244 | 186 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐵)) |
245 | 7, 244 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐵)) |
246 | 18, 21, 24, 42 | limcicciooub 38704 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐺 limℂ 𝐵)) |
247 | 245, 246 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (𝐺 limℂ 𝐵)) |
248 | 243, 247 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝐵) ∈ (𝐺 limℂ 𝐵)) |
249 | 101, 192 | cnplimc 23457 |
. . . . . . . . . . . 12
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐵 ∈ (𝐴[,]𝐵)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐵) ∈ (𝐺 limℂ 𝐵)))) |
250 | 132, 202,
249 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐵) ∈ (𝐺 limℂ 𝐵)))) |
251 | 42, 248, 250 | mpbir2and 959 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵)) |
252 | 251 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵)) |
253 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐵 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵)) |
254 | 253 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
255 | 254 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐵) →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
256 | 252, 255 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
257 | 200, 256 | jaodan 822 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
258 | 179, 257 | sylan2 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝐴, 𝐵}) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
259 | 178, 258 | jaodan 822 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
260 | 47, 259 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
261 | 260 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) |
262 | 101 | cnfldtopon 22396 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
263 | | resttopon 20775 |
. . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴[,]𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
264 | 262, 132,
263 | sylancr 694 |
. . . 4
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) |
265 | | cncnp 20894 |
. . . 4
⊢
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐺 ∈
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
266 | 264, 262,
265 | sylancl 693 |
. . 3
⊢ (𝜑 → (𝐺 ∈
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
267 | 42, 261, 266 | mpbir2and 959 |
. 2
⊢ (𝜑 → 𝐺 ∈
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn
(TopOpen‘ℂfld))) |
268 | 101, 192,
107 | cncfcn 22520 |
. . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴[,]𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn
(TopOpen‘ℂfld))) |
269 | 132, 100,
268 | sylancl 693 |
. 2
⊢ (𝜑 → ((𝐴[,]𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn
(TopOpen‘ℂfld))) |
270 | 267, 269 | eleqtrrd 2691 |
1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |