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 φ A
cncfuni.f φ F : A
cncfuni.auni φ A B
cncfuni.opn φ b B A b TopOpen fld 𝑡 A
cncfuni.fcn φ b B F b : A b cn
Assertion cncfuni φ F : A cn

Proof

Step Hyp Ref Expression
1 cncfuni.acn φ A
2 cncfuni.f φ F : A
3 cncfuni.auni φ A B
4 cncfuni.opn φ b B A b TopOpen fld 𝑡 A
5 cncfuni.fcn φ b B F b : A b cn
6 3 sselda φ x A x B
7 eluni2 x B b B x b
8 6 7 sylib φ x A b B x b
9 simp1l φ x A b B x b φ
10 simp2 φ x A b B x b b B
11 elin x A b x A x b
12 11 biimpri x A x b x A b
13 12 adantll φ x A x b x A b
14 13 3adant2 φ x A b B x b x A b
15 2 fdmd φ dom F = A
16 15 ineq2d φ b dom F = b A
17 incom b A = A b
18 16 17 eqtr2di φ A b = b dom F
19 18 reseq2d φ F A b = F b dom F
20 frel F : A Rel F
21 2 20 syl φ Rel F
22 resindm Rel F F b dom F = F b
23 21 22 syl φ F b dom F = F b
24 19 23 eqtrd φ F A b = F b
25 inss1 A b A
26 25 a1i φ A b A
27 26 1 sstrd φ A b
28 ssidd φ
29 eqid TopOpen fld = TopOpen fld
30 eqid TopOpen fld 𝑡 A b = TopOpen fld 𝑡 A b
31 29 cnfldtop TopOpen fld Top
32 unicntop = TopOpen fld
33 32 restid TopOpen fld Top TopOpen fld 𝑡 = TopOpen fld
34 31 33 ax-mp TopOpen fld 𝑡 = TopOpen fld
35 34 eqcomi TopOpen fld = TopOpen fld 𝑡
36 29 30 35 cncfcn A b A b cn = TopOpen fld 𝑡 A b Cn TopOpen fld
37 27 28 36 syl2anc φ A b cn = TopOpen fld 𝑡 A b Cn TopOpen fld
38 37 eqcomd φ TopOpen fld 𝑡 A b Cn TopOpen fld = A b cn
39 24 38 eleq12d φ F A b TopOpen fld 𝑡 A b Cn TopOpen fld F b : A b cn
40 39 adantr φ b B F A b TopOpen fld 𝑡 A b Cn TopOpen fld F b : A b cn
41 5 40 mpbird φ b B F A b TopOpen fld 𝑡 A b Cn TopOpen fld
42 41 3adant3 φ b B x A b F A b TopOpen fld 𝑡 A b Cn TopOpen fld
43 29 cnfldtopon TopOpen fld TopOn
44 43 a1i φ TopOpen fld TopOn
45 resttopon TopOpen fld TopOn A b TopOpen fld 𝑡 A b TopOn A b
46 44 27 45 syl2anc φ TopOpen fld 𝑡 A b TopOn A b
47 46 3ad2ant1 φ b B x A b TopOpen fld 𝑡 A b TopOn A b
48 43 a1i φ b B x A b TopOpen fld TopOn
49 cncnp TopOpen fld 𝑡 A b TopOn A b TopOpen fld TopOn F A b TopOpen fld 𝑡 A b Cn TopOpen fld F A b : A b x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x
50 47 48 49 syl2anc φ b B x A b F A b TopOpen fld 𝑡 A b Cn TopOpen fld F A b : A b x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x
51 42 50 mpbid φ b B x A b F A b : A b x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x
52 51 simprd φ b B x A b x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x
53 simp3 φ b B x A b x A b
54 rspa x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x
55 52 53 54 syl2anc φ b B x A b F A b TopOpen fld 𝑡 A b CnP TopOpen fld x
56 31 a1i φ TopOpen fld Top
57 cnex V
58 57 ssex A A V
59 1 58 syl φ A V
60 restabs TopOpen fld Top A b A A V TopOpen fld 𝑡 A 𝑡 A b = TopOpen fld 𝑡 A b
61 56 26 59 60 syl3anc φ TopOpen fld 𝑡 A 𝑡 A b = TopOpen fld 𝑡 A b
62 61 eqcomd φ TopOpen fld 𝑡 A b = TopOpen fld 𝑡 A 𝑡 A b
63 62 oveq1d φ TopOpen fld 𝑡 A b CnP TopOpen fld = TopOpen fld 𝑡 A 𝑡 A b CnP TopOpen fld
64 63 fveq1d φ TopOpen fld 𝑡 A b CnP TopOpen fld x = TopOpen fld 𝑡 A 𝑡 A b CnP TopOpen fld x
65 64 3ad2ant1 φ b B x A b TopOpen fld 𝑡 A b CnP TopOpen fld x = TopOpen fld 𝑡 A 𝑡 A b CnP TopOpen fld x
66 55 65 eleqtrd φ b B x A b F A b TopOpen fld 𝑡 A 𝑡 A b CnP TopOpen fld x
67 resttop TopOpen fld Top A V TopOpen fld 𝑡 A Top
68 56 59 67 syl2anc φ TopOpen fld 𝑡 A Top
69 68 3ad2ant1 φ b B x A b TopOpen fld 𝑡 A Top
70 32 restuni TopOpen fld Top A A = TopOpen fld 𝑡 A
71 56 1 70 syl2anc φ A = TopOpen fld 𝑡 A
72 26 71 sseqtrd φ A b TopOpen fld 𝑡 A
73 72 3ad2ant1 φ b B x A b A b TopOpen fld 𝑡 A
74 4 3adant3 φ b B x A b A b TopOpen fld 𝑡 A
75 eqid TopOpen fld 𝑡 A = TopOpen fld 𝑡 A
76 75 isopn3 TopOpen fld 𝑡 A Top A b TopOpen fld 𝑡 A A b TopOpen fld 𝑡 A int TopOpen fld 𝑡 A A b = A b
77 69 73 76 syl2anc φ b B x A b A b TopOpen fld 𝑡 A int TopOpen fld 𝑡 A A b = A b
78 74 77 mpbid φ b B x A b int TopOpen fld 𝑡 A A b = A b
79 78 eqcomd φ b B x A b A b = int TopOpen fld 𝑡 A A b
80 53 79 eleqtrd φ b B x A b x int TopOpen fld 𝑡 A A b
81 71 feq2d φ F : A F : TopOpen fld 𝑡 A
82 2 81 mpbid φ F : TopOpen fld 𝑡 A
83 82 3ad2ant1 φ b B x A b F : TopOpen fld 𝑡 A
84 75 32 cnprest TopOpen fld 𝑡 A Top A b TopOpen fld 𝑡 A x int TopOpen fld 𝑡 A A b F : TopOpen fld 𝑡 A F TopOpen fld 𝑡 A CnP TopOpen fld x F A b TopOpen fld 𝑡 A 𝑡 A b CnP TopOpen fld x
85 69 73 80 83 84 syl22anc φ b B x A b F TopOpen fld 𝑡 A CnP TopOpen fld x F A b TopOpen fld 𝑡 A 𝑡 A b CnP TopOpen fld x
86 66 85 mpbird φ b B x A b F TopOpen fld 𝑡 A CnP TopOpen fld x
87 9 10 14 86 syl3anc φ x A b B x b F TopOpen fld 𝑡 A CnP TopOpen fld x
88 87 rexlimdv3a φ x A b B x b F TopOpen fld 𝑡 A CnP TopOpen fld x
89 8 88 mpd φ x A F TopOpen fld 𝑡 A CnP TopOpen fld x
90 89 ralrimiva φ x A F TopOpen fld 𝑡 A CnP TopOpen fld x
91 resttopon TopOpen fld TopOn A TopOpen fld 𝑡 A TopOn A
92 44 1 91 syl2anc φ TopOpen fld 𝑡 A TopOn A
93 cncnp TopOpen fld 𝑡 A TopOn A TopOpen fld TopOn F TopOpen fld 𝑡 A Cn TopOpen fld F : A x A F TopOpen fld 𝑡 A CnP TopOpen fld x
94 92 44 93 syl2anc φ F TopOpen fld 𝑡 A Cn TopOpen fld F : A x A F TopOpen fld 𝑡 A CnP TopOpen fld x
95 2 90 94 mpbir2and φ F TopOpen fld 𝑡 A Cn TopOpen fld
96 eqid TopOpen fld 𝑡 A = TopOpen fld 𝑡 A
97 29 96 35 cncfcn A A cn = TopOpen fld 𝑡 A Cn TopOpen fld
98 1 28 97 syl2anc φ A cn = TopOpen fld 𝑡 A Cn TopOpen fld
99 98 eqcomd φ TopOpen fld 𝑡 A Cn TopOpen fld = A cn
100 95 99 eleqtrd φ F : A cn