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	$$⊢\mathrm{Rel}{CHil}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		hlobn	$$⊢x\in {CHil}_{\mathrm{OLD}}\to x\in \mathrm{CBan}$$
2	1	ssriv	$$⊢{CHil}_{\mathrm{OLD}}\subseteq \mathrm{CBan}$$
3		bnrel	$$⊢\mathrm{Rel}\mathrm{CBan}$$
4		relss	$$⊢{CHil}_{\mathrm{OLD}}\subseteq \mathrm{CBan}\to \left(\mathrm{Rel}\mathrm{CBan}\to \mathrm{Rel}{CHil}_{\mathrm{OLD}}\right)$$
5	2 3 4	mp2	$$⊢\mathrm{Rel}{CHil}_{\mathrm{OLD}}$$