Description: Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | chcompl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isch3 | |
|
2 | 1 | simprbi | |
3 | feq1 | |
|
4 | breq1 | |
|
5 | 4 | rexbidv | |
6 | 3 5 | imbi12d | |
7 | 6 | rspccv | |
8 | 2 7 | syl | |
9 | 8 | 3imp | |