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 = { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbo	⊢ BndLinOp
1		vt	⊢ 𝑡
2		clo	⊢ LinOp
3		cnop	⊢ normop
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( normop ‘ 𝑡 )
6		clt	⊢ <
7		cpnf	⊢ +∞
8	5 7 6	wbr	⊢ ( normop ‘ 𝑡 ) < +∞
9	8 1 2	crab	⊢ { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }
10	0 9	wceq	⊢ BndLinOp = { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }