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 frel 
 |-  ( F : A --> CC -> Rel F )
21 2 20 syl 
 |-  ( ph -> Rel F )
22 resindm 
 |-  ( Rel F -> ( F |` ( b i^i dom F ) ) = ( F |` b ) )
23 21 22 syl 
 |-  ( ph -> ( F |` ( b i^i dom F ) ) = ( F |` b ) )
24 19 23 eqtrd 
 |-  ( ph -> ( F |` ( A i^i b ) ) = ( F |` b ) )
25 inss1 
 |-  ( A i^i b ) C_ A
26 25 a1i 
 |-  ( ph -> ( A i^i b ) C_ A )
27 26 1 sstrd 
 |-  ( ph -> ( A i^i b ) C_ CC )
28 ssidd 
 |-  ( ph -> CC C_ CC )
29 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
30 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) = ( ( TopOpen ` CCfld ) |`t ( A i^i b ) )
31 29 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
32 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
33 32 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
34 31 33 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
35 34 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
36 29 30 35 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 ) ) )
37 27 28 36 syl2anc 
 |-  ( ph -> ( ( A i^i b ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) Cn ( TopOpen ` CCfld ) ) )
38 37 eqcomd 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) Cn ( TopOpen ` CCfld ) ) = ( ( A i^i b ) -cn-> CC ) )
39 24 38 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 ) ) )
40 39 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 ) ) )
41 5 40 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( F |` ( A i^i b ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) Cn ( TopOpen ` CCfld ) ) )
42 41 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 ) ) )
43 29 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
44 43 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
45 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 ) ) )
46 44 27 45 syl2anc 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) e. ( TopOn ` ( A i^i b ) ) )
47 46 3ad2ant1 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) e. ( TopOn ` ( A i^i b ) ) )
48 43 a1i 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
49 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 ) ) ) )
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 ) ) 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 ) ) ) )
51 42 50 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 ) ) )
52 51 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 ) )
53 simp3 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> x e. ( A i^i b ) )
54 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 ) )
55 52 53 54 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 ) )
56 31 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
57 cnex 
 |-  CC e. _V
58 57 ssex 
 |-  ( A C_ CC -> A e. _V )
59 1 58 syl 
 |-  ( ph -> A e. _V )
60 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 ) ) )
61 56 26 59 60 syl3anc 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t A ) |`t ( A i^i b ) ) = ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) )
62 61 eqcomd 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) = ( ( ( TopOpen ` CCfld ) |`t A ) |`t ( A i^i b ) ) )
63 62 oveq1d 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t ( A i^i b ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( ( TopOpen ` CCfld ) |`t A ) |`t ( A i^i b ) ) CnP ( TopOpen ` CCfld ) ) )
64 63 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 ) )
65 64 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 ) )
66 55 65 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 ) )
67 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ A e. _V ) -> ( ( TopOpen ` CCfld ) |`t A ) e. Top )
68 56 59 67 syl2anc 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t A ) e. Top )
69 68 3ad2ant1 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( ( TopOpen ` CCfld ) |`t A ) e. Top )
70 32 restuni 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ A C_ CC ) -> A = U. ( ( TopOpen ` CCfld ) |`t A ) )
71 56 1 70 syl2anc 
 |-  ( ph -> A = U. ( ( TopOpen ` CCfld ) |`t A ) )
72 26 71 sseqtrd 
 |-  ( ph -> ( A i^i b ) C_ U. ( ( TopOpen ` CCfld ) |`t A ) )
73 72 3ad2ant1 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( A i^i b ) C_ U. ( ( TopOpen ` CCfld ) |`t A ) )
74 4 3adant3 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( A i^i b ) e. ( ( TopOpen ` CCfld ) |`t A ) )
75 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t A ) = U. ( ( TopOpen ` CCfld ) |`t A )
76 75 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 ) ) )
77 69 73 76 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 ) ) )
78 74 77 mpbid 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t A ) ) ` ( A i^i b ) ) = ( A i^i b ) )
79 78 eqcomd 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> ( A i^i b ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t A ) ) ` ( A i^i b ) ) )
80 53 79 eleqtrd 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t A ) ) ` ( A i^i b ) ) )
81 71 feq2d 
 |-  ( ph -> ( F : A --> CC <-> F : U. ( ( TopOpen ` CCfld ) |`t A ) --> CC ) )
82 2 81 mpbid 
 |-  ( ph -> F : U. ( ( TopOpen ` CCfld ) |`t A ) --> CC )
83 82 3ad2ant1 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> F : U. ( ( TopOpen ` CCfld ) |`t A ) --> CC )
84 75 32 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 ) ) )
85 69 73 80 83 84 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 ) ) )
86 66 85 mpbird 
 |-  ( ( ph /\ b e. B /\ x e. ( A i^i b ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
87 9 10 14 86 syl3anc 
 |-  ( ( ( ph /\ x e. A ) /\ b e. B /\ x e. b ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
88 87 rexlimdv3a 
 |-  ( ( ph /\ x e. A ) -> ( E. b e. B x e. b -> F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) ) )
89 8 88 mpd 
 |-  ( ( ph /\ x e. A ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
90 89 ralrimiva 
 |-  ( ph -> A. x e. A F e. ( ( ( ( TopOpen ` CCfld ) |`t A ) CnP ( TopOpen ` CCfld ) ) ` x ) )
91 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ A C_ CC ) -> ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) )
92 44 1 91 syl2anc 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t A ) e. ( TopOn ` A ) )
93 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 ) ) ) )
94 92 44 93 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 ) ) ) )
95 2 90 94 mpbir2and 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
96 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t A ) = ( ( TopOpen ` CCfld ) |`t A )
97 29 96 35 cncfcn 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( A -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
98 1 28 97 syl2anc 
 |-  ( ph -> ( A -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) )
99 98 eqcomd 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( TopOpen ` CCfld ) ) = ( A -cn-> CC ) )
100 95 99 eleqtrd 
 |-  ( ph -> F e. ( A -cn-> CC ) )