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⁡Df:ℕ⟶X→f∈dom⁡⇝t⁡J
8 7 mptru ⊢D∈CMet⁡X↔∀f∈Cau⁡Df:ℕ⟶X→f∈dom⁡⇝t⁡J
9 3 ex ⊢f∈Cau⁡D→f:ℕ⟶X→f∈dom⁡⇝t⁡J
10 8 9 mprgbir ⊢D∈CMet⁡X