This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rrncms

Description: Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis rrncms.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
Assertion rrncms ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( CMet ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 rrncms.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
3 eqid ⊢ ( MetOpen ‘ ( ℝn ‘ 𝐼 ) ) = ( MetOpen ‘ ( ℝn ‘ 𝐼 ) )
4 simpll ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ) ∧ 𝑓 : ℕ ⟶ 𝑋 ) → 𝐼 ∈ Fin )
5 simplr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ) ∧ 𝑓 : ℕ ⟶ 𝑋 ) → 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) )
6 simpr ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ) ∧ 𝑓 : ℕ ⟶ 𝑋 ) → 𝑓 : ℕ ⟶ 𝑋 )
7 eqid ⊢ ( 𝑚 ∈ 𝐼 ↦ ( ⇝ ‘ ( 𝑡 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑡 ) ‘ 𝑚 ) ) ) ) = ( 𝑚 ∈ 𝐼 ↦ ( ⇝ ‘ ( 𝑡 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑡 ) ‘ 𝑚 ) ) ) )
8 1 2 3 4 5 6 7 rrncmslem ⊢ ( ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ) ∧ 𝑓 : ℕ ⟶ 𝑋 ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( ℝn ‘ 𝐼 ) ) ) )
9 8 ex ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ) → ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( ℝn ‘ 𝐼 ) ) ) ) )
10 9 ralrimiva ⊢ ( 𝐼 ∈ Fin → ∀ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( ℝn ‘ 𝐼 ) ) ) ) )
11 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
12 1zzd ⊢ ( 𝐼 ∈ Fin → 1 ∈ ℤ )
13 1 rrnmet ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )
14 11 3 12 13 iscmet3 ⊢ ( 𝐼 ∈ Fin → ( ( ℝn ‘ 𝐼 ) ∈ ( CMet ‘ 𝑋 ) ↔ ∀ 𝑓 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( ℝn ‘ 𝐼 ) ) ) ) ) )
15 10 14 mpbird ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( CMet ‘ 𝑋 ) )