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


 |-  ( x e. CHilOLD -> x e. CBan )
 |-  CHilOLD C_ CBan
 |-  Rel CBan
 |-  ( CHilOLD C_ CBan -> ( Rel CBan -> Rel CHilOLD ) )
 |-  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