Metamath Proof Explorer

Theorem iscmet3i

Description: Properties that determine a complete metric space. (Contributed by NM, 15-Apr-2007) (Revised by Mario Carneiro, 5-May-2014)

Ref Expression
Hypotheses iscmet3i.2 ⊢ J = MetOpen ⁡ D
iscmet3i.3 ⊢ D ∈ Met ⁡ X
iscmet3i.4 ⊢ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ J
Assertion iscmet3i ⊢ D ∈ CMet ⁡ X

Proof

Step Hyp Ref Expression
1 iscmet3i.2 ⊢ J = MetOpen ⁡ D
2 iscmet3i.3 ⊢ D ∈ Met ⁡ X
3 iscmet3i.4 ⊢ f ∈ Cau ⁡ D ∧ f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ J
4 nnuz ⊢ ℕ = ℤ ≥ 1
5 1zzd ⊢ ⊤ → 1 ∈ ℤ
6 2 a1i ⊢ ⊤ → D ∈ Met ⁡ X
7 4 1 5 6 iscmet3 ⊢ ⊤ → D ∈ CMet ⁡ X ↔ ∀ f ∈ Cau ⁡ D f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ J
8 7 mptru ⊢ D ∈ CMet ⁡ X ↔ ∀ f ∈ Cau ⁡ D f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ J
9 3 ex ⊢ f ∈ Cau ⁡ D → f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ J
10 8 9 mprgbir ⊢ D ∈ CMet ⁡ X