| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cncfuni.f | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 2 |  | cncfuni.auni | . . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵) | 
| 3 | 2 | sselda 3982 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ 𝐵) | 
| 4 |  | eluni2 4910 | . . . . . 6
⊢ (𝑥 ∈ ∪ 𝐵
↔ ∃𝑏 ∈
𝐵 𝑥 ∈ 𝑏) | 
| 5 | 3, 4 | sylib 218 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏) | 
| 6 |  | simp1l 1197 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝜑) | 
| 7 |  | simp2 1137 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝑏 ∈ 𝐵) | 
| 8 |  | elin 3966 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∩ 𝑏) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏)) | 
| 9 | 8 | biimpri 228 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏)) | 
| 10 | 9 | adantll 714 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏)) | 
| 11 | 10 | 3adant2 1131 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏)) | 
| 12 |  | cncfuni.fcn | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ)) | 
| 13 | 1 | fdmd 6745 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐹 = 𝐴) | 
| 14 | 13 | ineq2d 4219 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑏 ∩ dom 𝐹) = (𝑏 ∩ 𝐴)) | 
| 15 |  | incom 4208 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∩ 𝐴) = (𝐴 ∩ 𝑏) | 
| 16 | 14, 15 | eqtr2di 2793 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∩ 𝑏) = (𝑏 ∩ dom 𝐹)) | 
| 17 | 16 | reseq2d 5996 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑏)) = (𝐹 ↾ (𝑏 ∩ dom 𝐹))) | 
| 18 |  | frel 6740 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝐴⟶ℂ → Rel 𝐹) | 
| 19 | 1, 18 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Rel 𝐹) | 
| 20 |  | resindm 6047 | . . . . . . . . . . . . . . . . . 18
⊢ (Rel
𝐹 → (𝐹 ↾ (𝑏 ∩ dom 𝐹)) = (𝐹 ↾ 𝑏)) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 ↾ (𝑏 ∩ dom 𝐹)) = (𝐹 ↾ 𝑏)) | 
| 22 | 17, 21 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑏)) = (𝐹 ↾ 𝑏)) | 
| 23 |  | inss1 4236 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴 | 
| 24 | 23 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ 𝐴) | 
| 25 |  | cncfuni.acn | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 26 | 24, 25 | sstrd 3993 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ ℂ) | 
| 27 |  | ssidd 4006 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 28 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 29 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld)
↾t (𝐴
∩ 𝑏)) | 
| 30 | 28 | cnfldtop 24805 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 31 |  | unicntop 24807 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 32 | 31 | restid 17479 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) | 
| 33 | 30, 32 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) | 
| 34 | 33 | eqcomi 2745 | . . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 35 | 28, 29, 34 | cncfcn 24937 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∩ 𝑏) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴 ∩
𝑏)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) | 
| 36 | 26, 27, 35 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐴 ∩ 𝑏)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) | 
| 37 | 36 | eqcomd 2742 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
= ((𝐴 ∩ 𝑏)–cn→ℂ)) | 
| 38 | 22, 37 | eleq12d 2834 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))) | 
| 40 | 12, 39 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) | 
| 41 | 40 | 3adant3 1132 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) | 
| 42 | 28 | cnfldtopon 24804 | . . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 43 | 42 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) | 
| 44 |  | resttopon 23170 | . . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴 ∩ 𝑏) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏))) | 
| 45 | 43, 26, 44 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏))) | 
| 46 | 45 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏))) | 
| 47 | 42 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) | 
| 48 |  | cncnp 23289 | . . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)))) | 
| 49 | 46, 47, 48 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)))) | 
| 50 | 41, 49 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥))) | 
| 51 | 50 | simprd 495 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 52 |  | simp3 1138 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝑥 ∈ (𝐴 ∩ 𝑏)) | 
| 53 |  | rspa 3247 | . . . . . . . . . 10
⊢
((∀𝑥 ∈
(𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥) ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 54 | 51, 52, 53 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 55 | 30 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) | 
| 56 |  | cnex 11237 | . . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V | 
| 57 | 56 | ssex 5320 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ ℂ → 𝐴 ∈ V) | 
| 58 | 25, 57 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ V) | 
| 59 |  | restabs 23174 | . . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴 ∧ 𝐴 ∈ V) →
(((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld)
↾t (𝐴
∩ 𝑏))) | 
| 60 | 55, 24, 58, 59 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld)
↾t (𝐴
∩ 𝑏))) | 
| 61 | 60 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) = (((TopOpen‘ℂfld)
↾t 𝐴)
↾t (𝐴
∩ 𝑏))) | 
| 62 | 61 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))
= ((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))) | 
| 63 | 62 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝜑 →
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥) = (((((TopOpen‘ℂfld)
↾t 𝐴)
↾t (𝐴
∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 64 | 63 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥) = (((((TopOpen‘ℂfld)
↾t 𝐴)
↾t (𝐴
∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 65 | 54, 64 | eleqtrd 2842 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 66 |  | resttop 23169 | . . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ∈ V) →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top) | 
| 67 | 55, 58, 66 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top) | 
| 68 | 67 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top) | 
| 69 | 31 | restuni 23171 | . . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ⊆ ℂ) → 𝐴 = ∪
((TopOpen‘ℂfld) ↾t 𝐴)) | 
| 70 | 55, 25, 69 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = ∪
((TopOpen‘ℂfld) ↾t 𝐴)) | 
| 71 | 24, 70 | sseqtrd 4019 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) | 
| 72 | 71 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) | 
| 73 |  | cncfuni.opn | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴)) | 
| 74 | 73 | 3adant3 1132 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴)) | 
| 75 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝐴) =
∪ ((TopOpen‘ℂfld)
↾t 𝐴) | 
| 76 | 75 | isopn3 23075 | . . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) → ((𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏))) | 
| 77 | 68, 72, 76 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏))) | 
| 78 | 74, 77 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏)) | 
| 79 | 78 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) =
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏))) | 
| 80 | 52, 79 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝑥 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏))) | 
| 81 | 70 | feq2d 6721 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹:𝐴⟶ℂ ↔ 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ)) | 
| 82 | 1, 81 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ) | 
| 83 | 82 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ) | 
| 84 | 75, 31 | cnprest 23298 | . . . . . . . . 9
⊢
(((((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))‘𝑥))) | 
| 85 | 68, 72, 80, 83, 84 | syl22anc 838 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥) ↔ (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥))) | 
| 86 | 65, 85 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 87 | 6, 7, 11, 86 | syl3anc 1372 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 88 | 87 | rexlimdv3a 3158 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥))) | 
| 89 | 5, 88 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 90 | 89 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) | 
| 91 |  | resttopon 23170 | . . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝐴 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴)) | 
| 92 | 43, 25, 91 | syl2anc 584 | . . . 4
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴)) | 
| 93 |  | cncnp 23289 | . . . 4
⊢
((((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)))) | 
| 94 | 92, 43, 93 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)))) | 
| 95 | 1, 90, 94 | mpbir2and 713 | . 2
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝐴) Cn
(TopOpen‘ℂfld))) | 
| 96 |  | eqid 2736 | . . . . 5
⊢
((TopOpen‘ℂfld) ↾t 𝐴) =
((TopOpen‘ℂfld) ↾t 𝐴) | 
| 97 | 28, 96, 34 | cncfcn 24937 | . . . 4
⊢ ((𝐴 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝐴–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐴) Cn
(TopOpen‘ℂfld))) | 
| 98 | 25, 27, 97 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐴–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐴) Cn
(TopOpen‘ℂfld))) | 
| 99 | 98 | eqcomd 2742 | . 2
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld))
= (𝐴–cn→ℂ)) | 
| 100 | 95, 99 | eleqtrd 2842 | 1
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) |