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	$$⊢\phi \to A\subseteq ℂ$$
	cncfuni.f	$$⊢\phi \to F:A⟶ℂ$$
	cncfuni.auni	$$⊢\phi \to A\subseteq \bigcup B$$
	cncfuni.opn	$$⊢\left(\phi \wedge b\in B\right)\to A\cap b\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}A\right)$$
	cncfuni.fcn	$$⊢\left(\phi \wedge b\in B\right)\to \left({F\upharpoonright }_b\right):\left(A\cap b\right)\underset{cn}{⟶}ℂ$$
Assertion	cncfuni	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$

Proof

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