Theorem raddcn

Description: Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017)

	Ref	Expression
Hypothesis	raddcn.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	raddcn	$$⊢\left(x\in ℝ,y\in ℝ⟼x+y\right)\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		raddcn.1	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3	2	addcn	$$⊢+\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
4		ax-resscn	$$⊢ℝ\subseteq ℂ$$
5		xpss12	$$⊢\left(ℝ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to {ℝ}^2\subseteq ℂ\times ℂ$$
6	4 4 5	mp2an	$$⊢{ℝ}^2\subseteq ℂ\times ℂ$$
7	2	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
8	2	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
9	8	toponunii	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
10	7 7 9 9	txunii	$$⊢ℂ\times ℂ=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
11	10	cnrest	$$⊢\left(+\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge {ℝ}^2\subseteq ℂ\times ℂ\right)\to {+\upharpoonright }_{{ℝ}^2}\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){\upharpoonright }_{𝑡}{ℝ}^2\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
12	3 6 11	mp2an	$$⊢{+\upharpoonright }_{{ℝ}^2}\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){\upharpoonright }_{𝑡}{ℝ}^2\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
13		reex	$$⊢ℝ\in \mathrm{V}$$
14		txrest	$$⊢\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\right)\wedge \left(ℝ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\right)\to \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){\upharpoonright }_{𝑡}{ℝ}^2=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right){\times }_t\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)$$
15	7 7 13 13 14	mp4an	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){\upharpoonright }_{𝑡}{ℝ}^2=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right){\times }_t\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)$$
16	2	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
17	1 16	eqtr2i	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ=J$$
18	17 17	oveq12i	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right){\times }_t\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)=J{\times }_{t}J$$
19	15 18	eqtri	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){\upharpoonright }_{𝑡}{ℝ}^2=J{\times }_{t}J$$
20	19	oveq1i	$$⊢\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right){\upharpoonright }_{𝑡}{ℝ}^2\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
21	12 20	eleqtri	$$⊢{+\upharpoonright }_{{ℝ}^2}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
22		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
23		ffn	$$⊢+:ℂ\times ℂ⟶ℂ\to +Fn\left(ℂ\times ℂ\right)$$
24	22 23	ax-mp	$$⊢+Fn\left(ℂ\times ℂ\right)$$
25		fnssres	$$⊢\left(+Fn\left(ℂ\times ℂ\right)\wedge {ℝ}^2\subseteq ℂ\times ℂ\right)\to \left({+\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2$$
26	24 6 25	mp2an	$$⊢\left({+\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2$$
27		fnov	$$⊢\left({+\upharpoonright }_{{ℝ}^2}\right)Fn{ℝ}^2\leftrightarrow {+\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼x\left({+\upharpoonright }_{{ℝ}^2}\right)y\right)$$
28	26 27	mpbi	$$⊢{+\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼x\left({+\upharpoonright }_{{ℝ}^2}\right)y\right)$$
29		ovres	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\left({+\upharpoonright }_{{ℝ}^2}\right)y=x+y$$
30	29	mpoeq3ia	$$⊢\left(x\in ℝ,y\in ℝ⟼x\left({+\upharpoonright }_{{ℝ}^2}\right)y\right)=\left(x\in ℝ,y\in ℝ⟼x+y\right)$$
31	28 30	eqtri	$$⊢{+\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼x+y\right)$$
32	31	rneqi	$$⊢\mathrm{ran}\left({+\upharpoonright }_{{ℝ}^2}\right)=\mathrm{ran}\left(x\in ℝ,y\in ℝ⟼x+y\right)$$
33		readdcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x+y\in ℝ$$
34	33	rgen2	$$⊢\forall x\in ℝ\forall y\in ℝx+y\in ℝ$$
35		eqid	$$⊢\left(x\in ℝ,y\in ℝ⟼x+y\right)=\left(x\in ℝ,y\in ℝ⟼x+y\right)$$
36	35	rnmposs	$$⊢\forall x\in ℝ\forall y\in ℝx+y\in ℝ\to \mathrm{ran}\left(x\in ℝ,y\in ℝ⟼x+y\right)\subseteq ℝ$$
37	34 36	ax-mp	$$⊢\mathrm{ran}\left(x\in ℝ,y\in ℝ⟼x+y\right)\subseteq ℝ$$
38	32 37	eqsstri	$$⊢\mathrm{ran}\left({+\upharpoonright }_{{ℝ}^2}\right)\subseteq ℝ$$
39		cnrest2	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge \mathrm{ran}\left({+\upharpoonright }_{{ℝ}^2}\right)\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left({+\upharpoonright }_{{ℝ}^2}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\leftrightarrow {+\upharpoonright }_{{ℝ}^2}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\right)\right)$$
40	8 38 4 39	mp3an	$$⊢{+\upharpoonright }_{{ℝ}^2}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\leftrightarrow {+\upharpoonright }_{{ℝ}^2}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\right)$$
41	21 40	mpbi	$$⊢{+\upharpoonright }_{{ℝ}^2}\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)\right)$$
42	17	oveq2i	$$⊢\left(J{\times }_{t}J\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ\right)=\left(J{\times }_{t}J\right)\mathrm{Cn}J$$
43	41 31 42	3eltr3i	$$⊢\left(x\in ℝ,y\in ℝ⟼x+y\right)\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$