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	⊢ Rel CPreHilOLD

Proof

Step	Hyp	Ref	Expression
1		phnv	⊢ ( 𝑥 ∈ CPreHilOLD → 𝑥 ∈ NrmCVec )
2	1	ssriv	⊢ CPreHilOLD ⊆ NrmCVec
3		nvrel	⊢ Rel NrmCVec
4		relss	⊢ ( CPreHilOLD ⊆ NrmCVec → ( Rel NrmCVec → Rel CPreHilOLD ) )
5	2 3 4	mp2	⊢ Rel CPreHilOLD