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 ⁡ D f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ J
10 9 adantl ⊢ D ∈ Met ⁡ X ∧ Cau ⁡ D ⊆ dom ⁡ ⇝t ⁡ J → ∀ f ∈ Cau ⁡ D f : ℕ ⟶ 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 ⁡ D f : ℕ ⟶ 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