Metamath Proof Explorer


Axiom ax-hcompl

Description: Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ax-hcompl
|- ( F e. Cauchy -> E. x e. ~H F ~~>v x )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF
 |-  F
1 ccauold
 |-  Cauchy
2 0 1 wcel
 |-  F e. Cauchy
3 vx
 |-  x
4 chba
 |-  ~H
5 chli
 |-  ~~>v
6 3 cv
 |-  x
7 0 6 5 wbr
 |-  F ~~>v x
8 7 3 4 wrex
 |-  E. x e. ~H F ~~>v x
9 2 8 wi
 |-  ( F e. Cauchy -> E. x e. ~H F ~~>v x )