Metamath Proof Explorer

Theorem cncfuni

Description: A complex function on a subset of the complex numbers is continuous if its domain is the union of relatively open subsets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfuni.acn ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
cncfuni.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
cncfuni.auni ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐵 )
cncfuni.opn ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
cncfuni.fcn ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ↾ 𝑏 ) ∈ ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) )
Assertion cncfuni ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 cncfuni.acn ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2 cncfuni.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3 cncfuni.auni ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐵 )
4 cncfuni.opn ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
5 cncfuni.fcn ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ↾ 𝑏 ) ∈ ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) )
6 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝐵 )
7 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 )
8 6 7 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 )
9 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏 ) → 𝜑 )
10 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏 ) → 𝑏 ∈ 𝐵 )
11 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏 ) )
12 11 biimpri ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏 ) → 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) )
13 12 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑏 ) → 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) )
14 13 3adant2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏 ) → 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) )
15 2 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
16 15 ineq2d ⊢ ( 𝜑 → ( 𝑏 ∩ dom 𝐹 ) = ( 𝑏 ∩ 𝐴 ) )
17 incom ⊢ ( 𝑏 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑏 )
18 16 17 eqtr2di ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) = ( 𝑏 ∩ dom 𝐹 ) )
19 18 reseq2d ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ↾ ( 𝑏 ∩ dom 𝐹 ) ) )
20 resindm ⊢ ( 𝐹 ↾ ( 𝑏 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑏 )
21 19 20 eqtrdi ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ↾ 𝑏 ) )
22 1 ssinss1d ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) ⊆ ℂ )
23 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
24 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
25 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) )
26 24 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
27 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
28 27 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
29 26 28 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
30 29 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
31 24 25 30 cncfcn ⊢ ( ( ( 𝐴 ∩ 𝑏 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
32 22 23 31 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
33 32 eqcomd ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) )
34 21 33 eleq12d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 ↾ 𝑏 ) ∈ ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 ↾ 𝑏 ) ∈ ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) ) )
36 5 35 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
37 36 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
38 24 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
39 38 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
40 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∩ 𝑏 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) )
41 39 22 40 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) )
42 41 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) )
43 38 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
44 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) : ( 𝐴 ∩ 𝑏 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
45 42 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) : ( 𝐴 ∩ 𝑏 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
46 37 45 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) : ( 𝐴 ∩ 𝑏 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
47 46 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
48 simp3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) )
49 rspa ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
50 47 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
51 26 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
52 inss1 ⊢ ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴
53 52 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴 )
54 cnex ⊢ ℂ ∈ V
55 54 ssex ⊢ ( 𝐴 ⊆ ℂ → 𝐴 ∈ V )
56 1 55 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
57 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴 ∧ 𝐴 ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) )
58 51 53 56 57 syl3anc ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) )
59 58 eqcomd ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) )
60 59 oveq1d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) )
61 60 fveq1d ⊢ ( 𝜑 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) = ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
62 61 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) = ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
63 50 62 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
64 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐴 ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top )
65 51 56 64 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top )
66 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top )
67 27 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐴 ⊆ ℂ ) → 𝐴 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
68 51 1 67 syl2anc ⊢ ( 𝜑 → 𝐴 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
69 53 68 sseqtrd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
70 69 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
71 4 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
72 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
73 72 isopn3 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top ∧ ( 𝐴 ∩ 𝑏 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) → ( ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐴 ∩ 𝑏 ) ) )
74 66 70 73 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐴 ∩ 𝑏 ) ) )
75 71 74 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐴 ∩ 𝑏 ) )
76 48 75 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) )
77 68 2 feq2dd ⊢ ( 𝜑 → 𝐹 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ⟶ ℂ )
78 77 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝐹 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ⟶ ℂ )
79 72 27 cnprest ⊢ ( ( ( ( ( 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 ) ) ‘ 𝑥 ) ) )
80 66 70 76 78 79 syl22anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
81 63 80 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
82 9 10 14 81 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
83 82 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
84 8 83 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
85 84 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
86 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
87 39 1 86 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
88 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
89 87 39 88 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
90 2 85 89 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
91 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
92 24 91 30 cncfcn ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
93 1 23 92 syl2anc ⊢ ( 𝜑 → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
94 90 93 eleqtrrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )