| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cncfiooicclem1.x | . . . 4
⊢
Ⅎ𝑥𝜑 | 
| 2 |  | limccl 25910 | . . . . . . 7
⊢ (𝐹 limℂ 𝐴) ⊆
ℂ | 
| 3 |  | cncfiooicclem1.r | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴)) | 
| 4 | 2, 3 | sselid 3981 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℂ) | 
| 5 | 4 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑥 = 𝐴) → 𝑅 ∈ ℂ) | 
| 6 |  | limccl 25910 | . . . . . . . 8
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ | 
| 7 |  | cncfiooicclem1.l | . . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵)) | 
| 8 | 6, 7 | sselid 3981 | . . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℂ) | 
| 9 | 8 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ) | 
| 10 |  | simplll 775 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝜑) | 
| 11 |  | orel1 889 | . . . . . . . . . . 11
⊢ (¬
𝑥 = 𝐴 → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵) → 𝑥 = 𝐵)) | 
| 12 | 11 | con3dimp 408 | . . . . . . . . . 10
⊢ ((¬
𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) | 
| 13 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 14 | 13 | elpr 4650 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴, 𝐵} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)) | 
| 15 | 12, 14 | sylnibr 329 | . . . . . . . . 9
⊢ ((¬
𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵}) | 
| 16 | 15 | adantll 714 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ¬ 𝑥 ∈ {𝐴, 𝐵}) | 
| 17 |  | simpllr 776 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 18 |  | cncfiooicclem1.a | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 19 | 18 | rexrd 11311 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 20 | 10, 19 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ∈
ℝ*) | 
| 21 |  | cncfiooicclem1.b | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 22 | 21 | rexrd 11311 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 23 | 10, 22 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐵 ∈
ℝ*) | 
| 24 |  | cncfiooicclem1.altb | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 25 | 18, 21, 24 | ltled 11409 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 26 | 10, 25 | syl 17 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝐴 ≤ 𝐵) | 
| 27 |  | prunioo 13521 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | 
| 28 | 20, 23, 26, 27 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | 
| 29 | 17, 28 | eleqtrrd 2844 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵})) | 
| 30 |  | elun 4153 | . . . . . . . . 9
⊢ (𝑥 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵})) | 
| 31 | 29, 30 | sylib 218 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵})) | 
| 32 |  | orel2 891 | . . . . . . . 8
⊢ (¬
𝑥 ∈ {𝐴, 𝐵} → ((𝑥 ∈ (𝐴(,)𝐵) ∨ 𝑥 ∈ {𝐴, 𝐵}) → 𝑥 ∈ (𝐴(,)𝐵))) | 
| 33 | 16, 31, 32 | sylc 65 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ (𝐴(,)𝐵)) | 
| 34 |  | cncfiooicclem1.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 35 |  | cncff 24919 | . . . . . . . . 9
⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ) | 
| 36 | 34, 35 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ) | 
| 37 | 36 | ffvelcdmda 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) | 
| 38 | 10, 33, 37 | syl2anc 584 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) ∈ ℂ) | 
| 39 | 9, 38 | ifclda 4561 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) ∈ ℂ) | 
| 40 | 5, 39 | ifclda 4561 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) | 
| 41 |  | cncfiooicclem1.g | . . . 4
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) | 
| 42 | 1, 40, 41 | fmptdf 7137 | . . 3
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) | 
| 43 |  | elun 4153 | . . . . . . 7
⊢ (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) | 
| 44 | 19, 22, 25, 27 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) = (𝐴[,]𝐵)) | 
| 45 | 44 | eleq2d 2827 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ((𝐴(,)𝐵) ∪ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵))) | 
| 46 | 43, 45 | bitr3id 285 | . . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵}) ↔ 𝑦 ∈ (𝐴[,]𝐵))) | 
| 47 | 46 | biimpar 477 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) | 
| 48 |  | ioossicc 13473 | . . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | 
| 49 |  | fssres 6774 | . . . . . . . . . . . . 13
⊢ ((𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ) | 
| 50 | 42, 48, 49 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)):(𝐴(,)𝐵)⟶ℂ) | 
| 51 | 50 | feqmptd 6977 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦))) | 
| 52 |  | nfmpt1 5250 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑥 ∈ (𝐴[,]𝐵) ↦ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) | 
| 53 | 41, 52 | nfcxfr 2903 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐺 | 
| 54 |  | nfcv 2905 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝐴(,)𝐵) | 
| 55 | 53, 54 | nfres 5999 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝐺 ↾ (𝐴(,)𝐵)) | 
| 56 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑦 | 
| 57 | 55, 56 | nffv 6916 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) | 
| 58 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝐺 ↾ (𝐴(,)𝐵)) | 
| 59 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝑥 | 
| 60 | 58, 59 | nffv 6916 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) | 
| 61 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦) = ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) | 
| 62 | 57, 60, 61 | cbvmpt 5253 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) | 
| 63 | 62 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑦)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥))) | 
| 64 |  | fvres 6925 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺‘𝑥)) | 
| 65 | 64 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐺‘𝑥)) | 
| 66 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) | 
| 67 | 48, 66 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴[,]𝐵)) | 
| 68 | 4 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑅 ∈ ℂ) | 
| 69 | 8 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ 𝑥 = 𝐵) → 𝐿 ∈ ℂ) | 
| 70 | 37 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) ∈ ℂ) | 
| 71 | 69, 70 | ifclda 4561 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) ∈ ℂ) | 
| 72 | 68, 71 | ifcld 4572 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) | 
| 73 | 41 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) ∈ ℂ) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) | 
| 74 | 67, 72, 73 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑥) = if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)))) | 
| 75 |  | elioo4g 13447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑥 ∈ ℝ)
∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) | 
| 76 | 75 | biimpi 216 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑥 ∈ ℝ)
∧ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) | 
| 77 | 76 | simpld 494 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑥 ∈
ℝ)) | 
| 78 | 77 | simp1d 1143 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 ∈
ℝ*) | 
| 79 |  | elioore 13417 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) | 
| 80 | 79 | rexrd 11311 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ*) | 
| 81 |  | eliooord 13446 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) | 
| 82 | 81 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝐴 < 𝑥) | 
| 83 |  | xrltne 13205 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ* ∧ 𝐴
< 𝑥) → 𝑥 ≠ 𝐴) | 
| 84 | 78, 80, 82, 83 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ≠ 𝐴) | 
| 85 | 84 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 𝐴) | 
| 86 | 85 | neneqd 2945 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ¬ 𝑥 = 𝐴) | 
| 87 | 86 | iffalsed 4536 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) | 
| 88 | 81 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 < 𝐵) | 
| 89 | 79, 88 | ltned 11397 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ≠ 𝐵) | 
| 90 | 89 | neneqd 2945 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ¬ 𝑥 = 𝐵) | 
| 91 | 90 | iffalsed 4536 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴(,)𝐵) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥)) | 
| 92 | 91 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥)) | 
| 93 | 87, 92 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = (𝐹‘𝑥)) | 
| 94 | 65, 74, 93 | 3eqtrd 2781 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥) = (𝐹‘𝑥)) | 
| 95 | 1, 94 | mpteq2da 5240 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ ((𝐺 ↾ (𝐴(,)𝐵))‘𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) | 
| 96 | 51, 63, 95 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) | 
| 97 | 36 | feqmptd 6977 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) | 
| 98 |  | ioosscn 13449 | . . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℂ | 
| 99 | 98 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) | 
| 100 |  | ssid 4006 | . . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ | 
| 101 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 102 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵)) | 
| 103 | 101 | cnfldtop 24804 | . . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 104 |  | unicntop 24806 | . . . . . . . . . . . . . . . 16
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 105 | 104 | restid 17478 | . . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) | 
| 106 | 103, 105 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) | 
| 107 | 106 | eqcomi 2746 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 108 | 101, 102,
107 | cncfcn 24936 | . . . . . . . . . . . 12
⊢ (((𝐴(,)𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 109 | 99, 100, 108 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴(,)𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 110 | 34, 97, 109 | 3eltr3d 2855 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 111 | 96, 110 | eqeltrd 2841 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 112 | 104 | restuni 23170 | . . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ ℂ) → (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵))) | 
| 113 | 103, 98, 112 | mp2an 692 | . . . . . . . . . 10
⊢ (𝐴(,)𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) | 
| 114 | 113 | cncnpi 23286 | . . . . . . . . 9
⊢ (((𝐺 ↾ (𝐴(,)𝐵)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) Cn (TopOpen‘ℂfld))
∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 115 | 111, 114 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 116 | 103 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
(TopOpen‘ℂfld) ∈ Top) | 
| 117 | 48 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) | 
| 118 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢ (𝐴[,]𝐵) ∈ V | 
| 119 | 118 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ∈ V) | 
| 120 |  | restabs 23173 | . . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) ∧ (𝐴[,]𝐵) ∈ V) →
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) | 
| 121 | 116, 117,
119, 120 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴(,)𝐵))) | 
| 122 | 121 | eqcomd 2743 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) = (((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵))) | 
| 123 | 122 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
(((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld)) =
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))) | 
| 124 | 123 | fveq1d 6908 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
((((TopOpen‘ℂfld) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = (((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 125 | 115, 124 | eleqtrd 2843 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 126 |  | resttop 23168 | . . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ∈ V) →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top) | 
| 127 | 103, 118,
126 | mp2an 692 | . . . . . . . . 9
⊢
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top | 
| 128 | 127 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ Top) | 
| 129 | 48 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) | 
| 130 | 18, 21 | iccssred 13474 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | 
| 131 |  | ax-resscn 11212 | . . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ | 
| 132 | 130, 131 | sstrdi 3996 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) | 
| 133 | 104 | restuni 23170 | . . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℂ) → (𝐴[,]𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) | 
| 134 | 103, 132,
133 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) = ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) | 
| 135 | 129, 134 | sseqtrd 4020 | . . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) | 
| 136 | 135 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))) | 
| 137 |  | retop 24782 | . . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top | 
| 138 | 137 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (topGen‘ran (,)) ∈
Top) | 
| 139 |  | ioossre 13448 | . . . . . . . . . . . . . . 15
⊢ (𝐴(,)𝐵) ⊆ ℝ | 
| 140 |  | difss 4136 | . . . . . . . . . . . . . . 15
⊢ (ℝ
∖ (𝐴[,]𝐵)) ⊆
ℝ | 
| 141 | 139, 140 | unssi 4191 | . . . . . . . . . . . . . 14
⊢ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ | 
| 142 | 141 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ) | 
| 143 |  | ssun1 4178 | . . . . . . . . . . . . . 14
⊢ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) | 
| 144 | 143 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) | 
| 145 |  | uniretop 24783 | . . . . . . . . . . . . . 14
⊢ ℝ =
∪ (topGen‘ran (,)) | 
| 146 | 145 | ntrss 23063 | . . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) → ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵)) ⊆
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) | 
| 147 | 138, 142,
144, 146 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵)) ⊆
((int‘(topGen‘ran (,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) | 
| 148 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴(,)𝐵)) | 
| 149 |  | ioontr 45524 | . . . . . . . . . . . . 13
⊢
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵) | 
| 150 | 148, 149 | eleqtrrdi 2852 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵))) | 
| 151 | 147, 150 | sseldd 3984 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵))))) | 
| 152 | 48, 148 | sselid 3981 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (𝐴[,]𝐵)) | 
| 153 | 151, 152 | elind 4200 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ (((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) | 
| 154 | 130 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 155 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) = ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) | 
| 156 | 145, 155 | restntr 23190 | . . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) | 
| 157 | 138, 154,
117, 156 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((int‘((topGen‘ran
(,)) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵)) = (((int‘(topGen‘ran
(,)))‘((𝐴(,)𝐵) ∪ (ℝ ∖ (𝐴[,]𝐵)))) ∩ (𝐴[,]𝐵))) | 
| 158 | 153, 157 | eleqtrrd 2844 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈ ((int‘((topGen‘ran (,))
↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵))) | 
| 159 |  | tgioo4 24826 | . . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 160 | 159 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (topGen‘ran (,)) =
((TopOpen‘ℂfld) ↾t
ℝ)) | 
| 161 | 160 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) = (((TopOpen‘ℂfld)
↾t ℝ) ↾t (𝐴[,]𝐵))) | 
| 162 | 103 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) | 
| 163 |  | reex 11246 | . . . . . . . . . . . . . . 15
⊢ ℝ
∈ V | 
| 164 | 163 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ∈
V) | 
| 165 |  | restabs 23173 | . . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ∈ V)
→ (((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) | 
| 166 | 162, 130,
164, 165 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t ℝ)
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) | 
| 167 | 161, 166 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → ((topGen‘ran (,))
↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵))) | 
| 168 | 167 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝜑 →
(int‘((topGen‘ran (,)) ↾t (𝐴[,]𝐵))) =
(int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))) | 
| 169 | 168 | fveq1d 6908 | . . . . . . . . . 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 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)))‘(𝐴(,)𝐵))) | 
| 172 | 134 | feq2d 6722 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺:(𝐴[,]𝐵)⟶ℂ ↔ 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ)) | 
| 173 | 42, 172 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ) | 
| 174 | 173 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐺:∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵))⟶ℂ) | 
| 175 |  | eqid 2737 | . . . . . . . . 9
⊢ ∪ ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) = ∪
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) | 
| 176 | 175, 104 | cnprest 23297 | . . . . . . . 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 839 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐺 ↾ (𝐴(,)𝐵)) ∈
(((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ↾t (𝐴(,)𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦))) | 
| 178 | 125, 177 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 179 |  | elpri 4649 | . . . . . . 7
⊢ (𝑦 ∈ {𝐴, 𝐵} → (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) | 
| 180 |  | iftrue 4531 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) | 
| 181 |  | lbicc2 13504 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 182 | 19, 22, 25, 181 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 183 | 41, 180, 182, 3 | fvmptd3 7039 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘𝐴) = 𝑅) | 
| 184 | 97 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)) = 𝐹) | 
| 185 | 96, 184 | eqtr2d 2778 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝐺 ↾ (𝐴(,)𝐵))) | 
| 186 | 185 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 limℂ 𝐴) = ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐴)) | 
| 187 | 3, 186 | eleqtrd 2843 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐴)) | 
| 188 | 18, 21, 24, 42 | limciccioolb 45636 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐴) = (𝐺 limℂ 𝐴)) | 
| 189 | 187, 188 | eleqtrd 2843 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ (𝐺 limℂ 𝐴)) | 
| 190 | 183, 189 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝐴) ∈ (𝐺 limℂ 𝐴)) | 
| 191 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) = ((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) | 
| 192 | 101, 191 | cnplimc 25922 | . . . . . . . . . . . 12
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐴) ∈ (𝐺 limℂ 𝐴)))) | 
| 193 | 132, 182,
192 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐴) ∈ (𝐺 limℂ 𝐴)))) | 
| 194 | 42, 190, 193 | mpbir2and 713 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴)) | 
| 195 | 194 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴)) | 
| 196 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐴 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴)) | 
| 197 | 196 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝑦 = 𝐴 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 198 | 197 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐴) →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐴) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 199 | 195, 198 | eleqtrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 200 | 180 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = 𝑅) | 
| 201 |  | eqtr2 2761 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐴) | 
| 202 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = 𝐴 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) = 𝑅) | 
| 203 | 202 | eqcomd 2743 | . . . . . . . . . . . . . . . . 17
⊢ (𝐵 = 𝐴 → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 204 | 201, 203 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → 𝑅 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 205 | 200, 204 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝐵 ∧ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 206 |  | iffalse 4534 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 = 𝐴 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) | 
| 207 | 206 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) | 
| 208 |  | iftrue 4531 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = 𝐿) | 
| 209 | 208 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥)) = 𝐿) | 
| 210 |  | df-ne 2941 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ≠ 𝐴 ↔ ¬ 𝑥 = 𝐴) | 
| 211 |  | pm13.18 3022 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 𝐵 ∧ 𝑥 ≠ 𝐴) → 𝐵 ≠ 𝐴) | 
| 212 | 210, 211 | sylan2br 595 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐵 ≠ 𝐴) | 
| 213 | 212 | neneqd 2945 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → ¬ 𝐵 = 𝐴) | 
| 214 | 213 | iffalsed 4536 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) | 
| 215 |  | eqid 2737 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐵 = 𝐵 | 
| 216 | 215 | iftruei 4532 | . . . . . . . . . . . . . . . . 17
⊢ if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)) = 𝐿 | 
| 217 | 214, 216 | eqtr2di 2794 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → 𝐿 = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 218 | 207, 209,
217 | 3eqtrd 2781 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝐵 ∧ ¬ 𝑥 = 𝐴) → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 219 | 205, 218 | pm2.61dan 813 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐴, 𝑅, if(𝑥 = 𝐵, 𝐿, (𝐹‘𝑥))) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 220 | 21 | leidd 11829 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≤ 𝐵) | 
| 221 | 18, 21, 21, 25, 220 | eliccd 45517 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) | 
| 222 | 216, 8 | eqeltrid 2845 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)) ∈ ℂ) | 
| 223 | 4, 222 | ifcld 4572 | . . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) ∈ ℂ) | 
| 224 | 41, 219, 221, 223 | fvmptd3 7039 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺‘𝐵) = if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)))) | 
| 225 | 18, 24 | gtned 11396 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ 𝐴) | 
| 226 | 225 | neneqd 2945 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐵 = 𝐴) | 
| 227 | 226 | iffalsed 4536 | . . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 = 𝐴, 𝑅, if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) = if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵))) | 
| 228 | 216 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → if(𝐵 = 𝐵, 𝐿, (𝐹‘𝐵)) = 𝐿) | 
| 229 | 224, 227,
228 | 3eqtrd 2781 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘𝐵) = 𝐿) | 
| 230 | 185 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐵)) | 
| 231 | 7, 230 | eleqtrd 2843 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐵)) | 
| 232 | 18, 21, 24, 42 | limcicciooub 45652 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐺 limℂ 𝐵)) | 
| 233 | 231, 232 | eleqtrd 2843 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (𝐺 limℂ 𝐵)) | 
| 234 | 229, 233 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝐵) ∈ (𝐺 limℂ 𝐵)) | 
| 235 | 101, 191 | cnplimc 25922 | . . . . . . . . . . . 12
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ 𝐵 ∈ (𝐴[,]𝐵)) → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐵) ∈ (𝐺 limℂ 𝐵)))) | 
| 236 | 132, 221,
235 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ (𝐺‘𝐵) ∈ (𝐺 limℂ 𝐵)))) | 
| 237 | 42, 234, 236 | mpbir2and 713 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵)) | 
| 238 | 237 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵)) | 
| 239 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐵 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵)) | 
| 240 | 239 | eqcomd 2743 | . . . . . . . . . 10
⊢ (𝑦 = 𝐵 →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 241 | 240 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝐵) →
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝐵) = ((((TopOpen‘ℂfld)
↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 242 | 238, 241 | eleqtrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 243 | 199, 242 | jaodan 960 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐵)) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 244 | 179, 243 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ {𝐴, 𝐵}) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 245 | 178, 244 | jaodan 960 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∨ 𝑦 ∈ {𝐴, 𝐵})) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 246 | 47, 245 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 247 | 246 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)) | 
| 248 | 101 | cnfldtopon 24803 | . . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 249 |  | resttopon 23169 | . . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴[,]𝐵) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) | 
| 250 | 248, 132,
249 | sylancr 587 | . . . 4
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵))) | 
| 251 |  | cncnp 23288 | . . . 4
⊢
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) ∈ (TopOn‘(𝐴[,]𝐵)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐺 ∈
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) | 
| 252 | 250, 248,
251 | sylancl 586 | . . 3
⊢ (𝜑 → (𝐺 ∈
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn (TopOpen‘ℂfld))
↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)𝐺 ∈
((((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) CnP
(TopOpen‘ℂfld))‘𝑦)))) | 
| 253 | 42, 247, 252 | mpbir2and 713 | . 2
⊢ (𝜑 → 𝐺 ∈
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 254 | 101, 191,
107 | cncfcn 24936 | . . 3
⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴[,]𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 255 | 132, 100,
254 | sylancl 586 | . 2
⊢ (𝜑 → ((𝐴[,]𝐵)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴[,]𝐵)) Cn
(TopOpen‘ℂfld))) | 
| 256 | 253, 255 | eleqtrrd 2844 | 1
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |