Metamath Proof Explorer


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 CHil OLD F Cau D F 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 CHil OLD D CMet BaseSet U
5 2 cmetcau D CMet BaseSet U F Cau D F dom t J
6 4 5 sylan U CHil OLD F Cau D F dom t J