Description: The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hlrel | |- Rel CHilOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlobn | |- ( x e. CHilOLD -> x e. CBan ) |
|
2 | 1 | ssriv | |- CHilOLD C_ CBan |
3 | bnrel | |- Rel CBan |
|
4 | relss | |- ( CHilOLD C_ CBan -> ( Rel CBan -> Rel CHilOLD ) ) |
|
5 | 2 3 4 | mp2 | |- Rel CHilOLD |