Metamath Proof Explorer
Description: The class of all normed complex vectors spaces is a relation.
(Contributed by NM, 14-Nov-2006) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
nvrel |
⊢ Rel NrmCVec |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nvss |
⊢ NrmCVec ⊆ ( CVecOLD × V ) |
2 |
|
relxp |
⊢ Rel ( CVecOLD × V ) |
3 |
|
relss |
⊢ ( NrmCVec ⊆ ( CVecOLD × V ) → ( Rel ( CVecOLD × V ) → Rel NrmCVec ) ) |
4 |
1 2 3
|
mp2 |
⊢ Rel NrmCVec |