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 ) |
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 ) |