Metamath Proof Explorer

Theorem raddcn

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

Ref Expression
Hypothesis raddcn.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
Assertion raddcn ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 raddcn.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 2 addcn ⊢ + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 xpss12 ⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) )
6 4 4 5 mp2an ⊢ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ )
7 2 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
8 2 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
9 8 toponunii ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
10 7 7 9 9 txunii ⊢ ( ℂ × ℂ ) = ∪ ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) )
11 10 cnrest ⊢ ( ( + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) ) → ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℝ × ℝ ) ) Cn ( TopOpen ‘ ℂfld ) ) )
12 3 6 11 mp2an ⊢ ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℝ × ℝ ) ) Cn ( TopOpen ‘ ℂfld ) )
13 reex ⊢ ℝ ∈ V
14 txrest ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( TopOpen ‘ ℂfld ) ∈ Top ) ∧ ( ℝ ∈ V ∧ ℝ ∈ V ) ) → ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℝ × ℝ ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
15 7 7 13 13 14 mp4an ⊢ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℝ × ℝ ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
16 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
17 1 16 eqtr2i ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) = 𝐽
18 17 17 oveq12i ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) = ( 𝐽 ×t 𝐽 )
19 15 18 eqtri ⊢ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℝ × ℝ ) ) = ( 𝐽 ×t 𝐽 )
20 19 oveq1i ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) ↾t ( ℝ × ℝ ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( 𝐽 ×t 𝐽 ) Cn ( TopOpen ‘ ℂfld ) )
21 12 20 eleqtri ⊢ ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( TopOpen ‘ ℂfld ) )
22 ax-addf ⊢ + : ( ℂ × ℂ ) ⟶ ℂ
23 ffn ⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → + Fn ( ℂ × ℂ ) )
24 22 23 ax-mp ⊢ + Fn ( ℂ × ℂ )
25 fnssres ⊢ ( ( + Fn ( ℂ × ℂ ) ∧ ( ℝ × ℝ ) ⊆ ( ℂ × ℂ ) ) → ( + ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) )
26 24 6 25 mp2an ⊢ ( + ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ )
27 fnov ⊢ ( ( + ↾ ( ℝ × ℝ ) ) Fn ( ℝ × ℝ ) ↔ ( + ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 ( + ↾ ( ℝ × ℝ ) ) 𝑦 ) ) )
28 26 27 mpbi ⊢ ( + ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 ( + ↾ ( ℝ × ℝ ) ) 𝑦 ) )
29 ovres ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( + ↾ ( ℝ × ℝ ) ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
30 29 mpoeq3ia ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 ( + ↾ ( ℝ × ℝ ) ) 𝑦 ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) )
31 28 30 eqtri ⊢ ( + ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) )
32 31 rneqi ⊢ ran ( + ↾ ( ℝ × ℝ ) ) = ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) )
33 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
34 33 rgen2 ⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 + 𝑦 ) ∈ ℝ
35 eqid ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) )
36 35 rnmposs ⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 + 𝑦 ) ∈ ℝ → ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ⊆ ℝ )
37 34 36 ax-mp ⊢ ran ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ⊆ ℝ
38 32 37 eqsstri ⊢ ran ( + ↾ ( ℝ × ℝ ) ) ⊆ ℝ
39 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( + ↾ ( ℝ × ℝ ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
40 8 38 4 39 mp3an ⊢ ( ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
41 21 40 mpbi ⊢ ( + ↾ ( ℝ × ℝ ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
42 17 oveq2i ⊢ ( ( 𝐽 ×t 𝐽 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) = ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
43 41 31 42 3eltr3i ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )