Definition df-chsup 10701

Description: Define the supremum of a set of Hilbert lattice elements. See chsupval2 10727 for its value and dfchsup2 10723 for an alternate definition. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice CH, to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupcl 10732.

Assertion

Ref	Expression
df-chsup	|- \/H = {<.x, y>. | (x C_ ~P~H /\ y = (_|_` (_|_` U.x)))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-chsup

Step	Hyp	Ref	Expression
1		chsup 10227	. 2 class \/H
2		vx	. . . . . 6 set x
3	2	cv 1135	. . . . 5 class x
4		chil 10212	. . . . . 6 class ~H
5	4	cpw 2856	. . . . 5 class ~P~H
6	3, 5	wss 2426	. . . 4 wff x C_ ~P~H
7		vy	. . . . . 6 set y
8	7	cv 1135	. . . . 5 class y
9	3	cuni 2999	. . . . . . 7 class U.x
10		cort 10223	. . . . . . 7 class _|_
11	9, 10	cfv 3809	. . . . . 6 class (_|_` U.x)
12	11, 10	cfv 3809	. . . . 5 class (_|_` (_|_` U.x))
13	8, 12	wceq 1136	. . . 4 wff y = (_|_` (_|_` U.x))
14	6, 13	wa 239	. . 3 wff (x C_ ~P~H /\ y = (_|_` (_|_` U.x)))
15	14, 2, 7	copab 3213	. 2 class {<.x, y>. | (x C_ ~P~H /\ y = (_|_` (_|_` U.x)))}
16	1, 15	wceq 1136	1 wff \/H = {<.x, y>. | (x C_ ~P~H /\ y = (_|_` (_|_` U.x)))}

This definition is referenced by:  dfchsup2 10723

Copyright terms: Public domain