Definition df-bn 23133

Description: Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)

Assertion

Ref	Expression
df-bn	|- Ban = { w e. (NrmVec i^i CMetSp ) | (Scalar ` w ) e. CMetSp }

Detailed syntax breakdown of Definition df-bn

Step	Hyp	Ref	Expression
1		cbn 23130	. 2 class Ban
2		vw	. . . . . 6 setvar w
3	2	cv 1482	. . . . 5 class w
4		csca 15944	. . . . 5 class Scalar
5	3, 4	cfv 5888	. . . 4 class (Scalar ` w )
6		ccms 23129	. . . 4 class CMetSp
7	5, 6	wcel 1990	. . 3 wff (Scalar ` w ) e. CMetSp
8		cnvc 22386	. . . 4 class NrmVec
9	8, 6	cin 3573	. . 3 class (NrmVec i^i CMetSp )
10	7, 2, 9	crab 2916	. 2 class { w e. (NrmVec i^i CMetSp ) | (Scalar ` w ) e. CMetSp }
11	1, 10	wceq 1483	1 wff Ban = { w e. (NrmVec i^i CMetSp ) | (Scalar ` w ) e. CMetSp }

This definition is referenced by:  isbn  23135