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	⊢ ( 𝑥 ∈ CHilOLD → 𝑥 ∈ CBan )
2	1	ssriv	⊢ CHilOLD ⊆ CBan
3		bnrel	⊢ Rel CBan
4		relss	⊢ ( CHilOLD ⊆ CBan → ( Rel CBan → Rel CHilOLD ) )
5	2 3 4	mp2	⊢ Rel CHilOLD