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

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
iscmet3i.3 ⊢ 𝐷 ∈ ( Met ‘ 𝑋 )
iscmet3i.4 ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝑋 ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
Assertion iscmet3i 𝐷 ∈ ( CMet ‘ 𝑋 )

Proof

Step Hyp Ref Expression
1 iscmet3i.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 iscmet3i.3 ⊢ 𝐷 ∈ ( Met ‘ 𝑋 )
3 iscmet3i.4 ⊢ ( ( 𝑓 ∈ ( Cau ‘ 𝐷 ) ∧ 𝑓 : ℕ ⟶ 𝑋 ) → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
4 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
5 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
6 2 a1i ⊢ ( ⊤ → 𝐷 ∈ ( Met ‘ 𝑋 ) )
7 4 1 5 6 iscmet3 ⊢ ( ⊤ → ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ∀ 𝑓 ∈ ( Cau ‘ 𝐷 ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) ) )
8 7 mptru ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ∀ 𝑓 ∈ ( Cau ‘ 𝐷 ) ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
9 3 ex ⊢ ( 𝑓 ∈ ( Cau ‘ 𝐷 ) → ( 𝑓 : ℕ ⟶ 𝑋 → 𝑓 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) ) )
10 8 9 mprgbir ⊢ 𝐷 ∈ ( CMet ‘ 𝑋 )