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	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	hlcompl.2	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
Assertion	hlcompl	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge F\in \mathrm{Cau}\left(D\right)\right)\to F\in \mathrm{dom}\underset{t}{⇝}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlcompl.1	$$⊢D=\mathrm{IndMet}\left(U\right)$$
2		hlcompl.2	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
3		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
4	3 1	hlcmet	$$⊢U\in {CHil}_{\mathrm{OLD}}\to D\in \mathrm{CMet}\left(\mathrm{BaseSet}\left(U\right)\right)$$
5	2	cmetcau	$$⊢\left(D\in \mathrm{CMet}\left(\mathrm{BaseSet}\left(U\right)\right)\wedge F\in \mathrm{Cau}\left(D\right)\right)\to F\in \mathrm{dom}\underset{t}{⇝}\left(J\right)$$
6	4 5	sylan	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge F\in \mathrm{Cau}\left(D\right)\right)\to F\in \mathrm{dom}\underset{t}{⇝}\left(J\right)$$