Metamath Proof Explorer

Theorem iscmet2

Description: A metric D is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of Kreyszig p. 28. (Contributed by NM, 7-Sep-2006) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis iscmet2.1 ⊢J=MetOpen⁡D
Assertion iscmet2 ⊢D∈CMet⁡X↔D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J

Proof

Step Hyp Ref Expression
1 iscmet2.1 ⊢J=MetOpen⁡D
2 cmetmet ⊢D∈CMet⁡X→D∈Met⁡X
3 1 cmetcau ⊢D∈CMet⁡X∧f∈Cau⁡D→f∈dom⁡⇝t⁡J
4 3 ex ⊢D∈CMet⁡X→f∈Cau⁡D→f∈dom⁡⇝t⁡J
5 4 ssrdv ⊢D∈CMet⁡X→Cau⁡D⊆dom⁡⇝t⁡J
6 2 5 jca ⊢D∈CMet⁡X→D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J
7 ssel2 ⊢Cau⁡D⊆dom⁡⇝t⁡J∧f∈Cau⁡D→f∈dom⁡⇝t⁡J
8 7 a1d ⊢Cau⁡D⊆dom⁡⇝t⁡J∧f∈Cau⁡D→f:ℕ⟶X→f∈dom⁡⇝t⁡J
9 8 ralrimiva ⊢Cau⁡D⊆dom⁡⇝t⁡J→∀f∈Cau⁡Df:ℕ⟶X→f∈dom⁡⇝t⁡J
10 9 adantl ⊢D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J→∀f∈Cau⁡Df:ℕ⟶X→f∈dom⁡⇝t⁡J
11 nnuz ⊢ℕ=ℤ≥1
12 1zzd ⊢D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J→1∈ℤ
13 simpl ⊢D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J→D∈Met⁡X
14 11 1 12 13 iscmet3 ⊢D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J→D∈CMet⁡X↔∀f∈Cau⁡Df:ℕ⟶X→f∈dom⁡⇝t⁡J
15 10 14 mpbird ⊢D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J→D∈CMet⁡X
16 6 15 impbii ⊢D∈CMet⁡X↔D∈Met⁡X∧Cau⁡D⊆dom⁡⇝t⁡J