This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 frel ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → Rel 𝐹 )
21 2 20 syl ⊢ ( 𝜑 → Rel 𝐹 )
22 resindm ⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( 𝑏 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑏 ) )
23 21 22 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑏 ∩ dom 𝐹 ) ) = ( 𝐹 ↾ 𝑏 ) )
24 19 23 eqtrd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐹 ↾ 𝑏 ) )
25 inss1 ⊢ ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴
26 25 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴 )
27 26 1 sstrd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) ⊆ ℂ )
28 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
29 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
30 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) )
31 29 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
32 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
33 32 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
34 31 33 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
35 34 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
36 29 30 35 cncfcn ⊢ ( ( ( 𝐴 ∩ 𝑏 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
37 27 28 36 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
38 37 eqcomd ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) )
39 24 38 eleq12d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 ↾ 𝑏 ) ∈ ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 ↾ 𝑏 ) ∈ ( ( 𝐴 ∩ 𝑏 ) –cn→ ℂ ) ) )
41 5 40 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
42 41 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) )
43 29 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
44 43 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
45 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∩ 𝑏 ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) )
46 44 27 45 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) )
47 46 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) )
48 43 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
49 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) ∈ ( TopOn ‘ ( 𝐴 ∩ 𝑏 ) ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) : ( 𝐴 ∩ 𝑏 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
50 47 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) : ( 𝐴 ∩ 𝑏 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
51 42 50 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) : ( 𝐴 ∩ 𝑏 ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
52 51 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
53 simp3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) )
54 rspa ⊢ ( ( ∀ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
55 52 53 54 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
56 31 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ Top )
57 cnex ⊢ ℂ ∈ V
58 57 ssex ⊢ ( 𝐴 ⊆ ℂ → 𝐴 ∈ V )
59 1 58 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
60 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝐴 ∩ 𝑏 ) ⊆ 𝐴 ∧ 𝐴 ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) )
61 56 26 59 60 syl3anc ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) )
62 61 eqcomd ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) )
63 62 oveq1d ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) )
64 63 fveq1d ⊢ ( 𝜑 → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) = ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
65 64 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) = ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
66 55 65 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
67 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐴 ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top )
68 56 59 67 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top )
69 68 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top )
70 32 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐴 ⊆ ℂ ) → 𝐴 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
71 56 1 70 syl2anc ⊢ ( 𝜑 → 𝐴 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
72 26 71 sseqtrd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑏 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
73 72 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
74 4 3adant3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) )
75 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
76 75 isopn3 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ Top ∧ ( 𝐴 ∩ 𝑏 ) ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) → ( ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐴 ∩ 𝑏 ) ) )
77 69 73 76 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( 𝐴 ∩ 𝑏 ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐴 ∩ 𝑏 ) ) )
78 74 77 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) = ( 𝐴 ∩ 𝑏 ) )
79 78 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐴 ∩ 𝑏 ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) )
80 53 79 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝑏 ) ) )
81 71 feq2d ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ℂ ↔ 𝐹 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ⟶ ℂ ) )
82 2 81 mpbid ⊢ ( 𝜑 → 𝐹 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ⟶ ℂ )
83 82 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝐹 : ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ⟶ ℂ )
84 75 32 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 ) ) ‘ 𝑥 ) ) )
85 69 73 80 83 84 syl22anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝑏 ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ↾t ( 𝐴 ∩ 𝑏 ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
86 66 85 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝑏 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
87 9 10 14 86 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
88 87 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) )
89 8 88 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
90 89 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) )
91 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐴 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
92 44 1 91 syl2anc ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
93 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
94 92 44 93 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑥 ) ) ) )
95 2 90 94 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
96 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
97 29 96 35 cncfcn ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
98 1 28 97 syl2anc ⊢ ( 𝜑 → ( 𝐴 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) )
99 98 eqcomd ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) Cn ( TopOpen ‘ ℂfld ) ) = ( 𝐴 –cn→ ℂ ) )
100 95 99 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )