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 = ( IndMet ` U )
	hlcompl.2	|- J = ( MetOpen ` D )
Assertion	hlcompl	|- ( ( U e. CHilOLD /\ F e. ( Cau ` D ) ) -> F e. dom ( ~~>t ` J ) )

Proof

Step	Hyp	Ref	Expression
1		hlcompl.1	|- D = ( IndMet ` U )
2		hlcompl.2	|- J = ( MetOpen ` D )
3		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
4	3 1	hlcmet	|- ( U e. CHilOLD -> D e. ( CMet ` ( BaseSet ` U ) ) )
5	2	cmetcau	|- ( ( D e. ( CMet ` ( BaseSet ` U ) ) /\ F e. ( Cau ` D ) ) -> F e. dom ( ~~>t ` J ) )
6	4 5	sylan	|- ( ( U e. CHilOLD /\ F e. ( Cau ` D ) ) -> F e. dom ( ~~>t ` J ) )