Definition df-ch 5127

Description: Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see closedsub 5128. From Definition of [Beran] p. 107. Alternate definitions are given by chcmh 5148 and dfch2 5254.

Assertion

Ref	Expression
df-ch	|- CH = {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}

Distinct variable group(s):   x,f,h

Detailed syntax breakdown of Definition df-ch

Step	Hyp	Ref	Expression
1		cch 4968	. 2 class CH
2		vh	. . . . . 6 set h
3	2	cv 1089	. . . . 5 class h
4		csh 4967	. . . . 5 class SH
5	3, 4	wcel 1092	. . . 4 wff h e. SH
6		cn 4093	. . . . . . . . 9 class NN
7		vf	. . . . . . . . . 10 set f
8	7	cv 1089	. . . . . . . . 9 class f
9	6, 3, 8	wf 2418	. . . . . . . 8 wff f:NN-->h
10		vx	. . . . . . . . . 10 set x
11	10	cv 1089	. . . . . . . . 9 class x
12		chli 4966	. . . . . . . . 9 class ~~>v
13	8, 11, 12	wbr 2054	. . . . . . . 8 wff f ~~>v x
14	9, 13	wa 196	. . . . . . 7 wff (f:NN-->h /\ f ~~>v x)
15	10, 2	wel 803	. . . . . . 7 wff x e. h
16	14, 15	wi 2	. . . . . 6 wff ((f:NN-->h /\ f ~~>v x) -> x e. h)
17	16, 10	wal 672	. . . . 5 wff A.x((f:NN-->h /\ f ~~>v x) -> x e. h)
18	17, 7	wal 672	. . . 4 wff A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h)
19	5, 18	wa 196	. . 3 wff (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))
20	19, 2	cab 1090	. 2 class {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}
21	1, 20	wceq 1091	1 wff CH = {h | (h e. SH /\ A.fA.x((f:NN-->h /\ f ~~>v x) -> x e. h))}

This definition is referenced by:  closedsub 5128  chsssh 5129

metamath.org