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 
|- ( ph -> A C_ CC )
cncfuni.f 
|- ( ph -> F : A --> CC )
cncfuni.auni 
|- ( ph -> A C_ U. B )
cncfuni.opn 
|- ( ( ph /\ b e. B ) -> ( A i^i b ) e. ( ( TopOpen ` CCfld ) |`t A ) )
cncfuni.fcn 
|- ( ( ph /\ b e. B ) -> ( F |` b ) e. ( ( A i^i b ) -cn-> CC ) )
Assertion cncfuni 
|- ( ph -> F e. ( A -cn-> CC ) )

Proof

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