Metamath Proof Explorer

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 
|- Rel CBan

Proof

Step Hyp Ref Expression
1 bnnv 
 |-  ( x e. CBan -> x e. NrmCVec )
2 1 ssriv 
 |-  CBan C_ NrmCVec
3 nvrel 
 |-  Rel NrmCVec
4 relss 
 |-  ( CBan C_ NrmCVec -> ( Rel NrmCVec -> Rel CBan ) )
5 2 3 4 mp2 
 |-  Rel CBan