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 ( ⇝𝑡 ‘ 𝐽 ) ) )