Definition df-bdop

Description: Define the set of bounded linear Hilbert space operators. (See df-hosum for definition of operator.) (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bdop	|- BndLinOp = { t e. LinOp | ( normop ` t ) < +oo }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbo	|- BndLinOp
1		vt	|- t
2		clo	|- LinOp
3		cnop	|- normop
4	1	cv	|- t
5	4 3	cfv	|- ( normop ` t )
6		clt	|- <
7		cpnf	|- +oo
8	5 7 6	wbr	|- ( normop ` t ) < +oo
9	8 1 2	crab	|- { t e. LinOp | ( normop ` t ) < +oo }
10	0 9	wceq	|- BndLinOp = { t e. LinOp | ( normop ` t ) < +oo }