Theorem cxpcncf2

Description: The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Assertion	cxpcncf2	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(x\in ℂ⟼A^x\right):ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
3	2	a1i	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
4		difss	$$⊢ℂ\setminus \left(\mathrm{-\infty },0\right]\subseteq ℂ$$
5		resttopon	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge ℂ\setminus \left(\mathrm{-\infty },0\right]\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\in \mathrm{TopOn}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)$$
6	2 4 5	mp2an	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\in \mathrm{TopOn}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)$$
7	6	a1i	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\in \mathrm{TopOn}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)$$
8		id	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)$$
9		snidg	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to A\in \left\{A\right\}$$
10	9	adantr	$$⊢\left(A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\wedge x\in ℂ\right)\to A\in \left\{A\right\}$$
11	10	fmpttd	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(x\in ℂ⟼A\right):ℂ⟶\left\{A\right\}$$
12		cnconst	$$⊢\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\in \mathrm{TopOn}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\right)\wedge \left(A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\wedge \left(x\in ℂ⟼A\right):ℂ⟶\left\{A\right\}\right)\right)\to \left(x\in ℂ⟼A\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\right)\right)$$
13	3 7 8 11 12	syl22anc	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(x\in ℂ⟼A\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\right)\right)$$
14	3	cnmptid	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(x\in ℂ⟼x\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
15		eqid	$$⊢ℂ\setminus \left(\mathrm{-\infty },0\right]=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
16		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)$$
17	15 1 16	cxpcn	$$⊢\left(y\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right),z\in ℂ⟼y^z\right)\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
18	17	a1i	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(y\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right),z\in ℂ⟼y^z\right)\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
19		oveq12	$$⊢\left(y=A\wedge z=x\right)\to y^z=A^x$$
20	3 13 14 7 3 18 19	cnmpt12	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(x\in ℂ⟼A^x\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
21		ssid	$$⊢ℂ\subseteq ℂ$$
22	2	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
23	1 22 22	cncfcn	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
24	21 21 23	mp2an	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
25	24	eqcomi	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=ℂ\underset{cn}{⟶}ℂ$$
26	25	a1i	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=ℂ\underset{cn}{⟶}ℂ$$
27	20 26	eleqtrd	$$⊢A\in \left(ℂ\setminus \left(\mathrm{-\infty },0\right]\right)\to \left(x\in ℂ⟼A^x\right):ℂ\underset{cn}{⟶}ℂ$$