Definition df-bn 22941

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 = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}

Detailed syntax breakdown of Definition df-bn

Step	Hyp	Ref	Expression
1		cbn 22938	. 2 class Ban
2		vw	. . . . . 6 setvar 𝑤
3	2	cv 1474	. . . . 5 class 𝑤
4		csca 15771	. . . . 5 class Scalar
5	3, 4	cfv 5804	. . . 4 class (Scalar‘𝑤)
6		ccms 22937	. . . 4 class CMetSp
7	5, 6	wcel 1977	. . 3 wff (Scalar‘𝑤) ∈ CMetSp
8		cnvc 22196	. . . 4 class NrmVec
9	8, 6	cin 3539	. . 3 class (NrmVec ∩ CMetSp)
10	7, 2, 9	crab 2900	. 2 class {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
11	1, 10	wceq 1475	1 wff Ban = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}

This definition is referenced by:  isbn  22943