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 )