Theorem bnrel

Description: The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	bnrel	$$⊢\mathrm{Rel}\mathrm{CBan}$$

Proof

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