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 ‘ 𝑋 )