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

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion iscmet2 ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 iscmet2.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 1 cmetcau ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑓 ∈ ( Cau ‘ 𝐷 ) ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
4 3 ex ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝑓 ∈ ( Cau ‘ 𝐷 ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
5 4 ssrdv ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) )
6 2 5 jca ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
7 ssel2 ⊢ ( ( ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ∧ 𝑓 ∈ ( Cau ‘ 𝐷 ) ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
8 7 a1d ⊢ ( ( ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ∧ 𝑓 ∈ ( Cau ‘ 𝐷 ) ) → ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
9 8 ralrimiva ⊢ ( ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) → ∀ 𝑓 ∈ ( Cau ‘ 𝐷 ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
10 9 adantl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) → ∀ 𝑓 ∈ ( Cau ‘ 𝐷 ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
11 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
12 1zzd ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) → 1 ∈ ℤ )
13 simpl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
14 11 1 12 13 iscmet3 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) → ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ∀ 𝑓 ∈ ( Cau ‘ 𝐷 ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) ) )
15 10 14 mpbird ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
16 6 15 impbii ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( Cau ‘ 𝐷 ) ⊆ dom ( ⇝𝑡 ‘ 𝐽 ) ) )