Theorem hlcompl

Description: Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007) (Revised by Mario Carneiro, 9-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlcompl.1	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	hlcompl.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	hlcompl	⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		hlcompl.1	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
2		hlcompl.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
4	3 1	hlcmet	⊢ ( 𝑈 ∈ CHilOLD → 𝐷 ∈ ( CMet ‘ ( BaseSet ‘ 𝑈 ) ) )
5	2	cmetcau	⊢ ( ( 𝐷 ∈ ( CMet ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )
6	4 5	sylan	⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐹 ∈ ( Cau ‘ 𝐷 ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )