Metamath Proof Explorer


Theorem hlrel

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

Proof

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