Theorem phrel

Description: The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	phrel	$$⊢\mathrm{Rel}{CPreHil}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		phnv	$$⊢x\in {CPreHil}_{\mathrm{OLD}}\to x\in \mathrm{NrmCVec}$$
2	1	ssriv	$$⊢{CPreHil}_{\mathrm{OLD}}\subseteq \mathrm{NrmCVec}$$
3		nvrel	$$⊢\mathrm{Rel}\mathrm{NrmCVec}$$
4		relss	$$⊢{CPreHil}_{\mathrm{OLD}}\subseteq \mathrm{NrmCVec}\to \left(\mathrm{Rel}\mathrm{NrmCVec}\to \mathrm{Rel}{CPreHil}_{\mathrm{OLD}}\right)$$
5	2 3 4	mp2	$$⊢\mathrm{Rel}{CPreHil}_{\mathrm{OLD}}$$