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	$⊢ φ \to A \subseteq ℂ$
	cncfuni.f	$⊢ φ \to F : A ⟶ ℂ$
	cncfuni.auni	$⊢ φ \to A \subseteq ⋃ B$
	cncfuni.opn	$⊢ (φ \land b \in B) \to A \cap b \in (TopOpen (ℂ_{fld}) ↾_{𝑡} A)$
	cncfuni.fcn	$⊢ (φ \land b \in B) \to ({F ↾}_{b}) : (A \cap b) \underset{cn}{⟶} ℂ$
Assertion	cncfuni	$⊢ φ \to F : A \underset{cn}{⟶} ℂ$

Proof

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

Metamath Proof Explorer

Theorem cncfuni

Proof