Definition df-chsup 9552

Description: Define the supremum of a set of Hilbert lattice elements. See chsupval2 9578 for its value and dfchsup2 9574 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 9583.

Assertion

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

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-chsup

Step	Hyp	Ref	Expression
1		chsup 9078	. 2 class \/H
2		vx	. . . . . 6 set x
3	2	cv 991	. . . . 5 class x
4		chil 9063	. . . . . 6 class H~
5	4	cpw 2458	. . . . 5 class P~H~
6	3, 5	wss 2099	. . . 4 wff x (_ P~H~
7		vy	. . . . . 6 set y
8	7	cv 991	. . . . 5 class y
9	3	cuni 2569	. . . . . . 7 class U.x
10		cort 9074	. . . . . . 7 class _|_
11	9, 10	cfv 3263	. . . . . 6 class (_|_` U.x)
12	11, 10	cfv 3263	. . . . 5 class (_|_` (_|_` U.x))
13	8, 12	wceq 992	. . . 4 wff y = (_|_` (_|_` U.x))
14	6, 13	wa 221	. . 3 wff (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))
15	14, 2, 7	copab 2740	. 2 class {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}
16	1, 15	wceq 992	1 wff \/H = {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}

This definition is referenced by:  dfchsup2 9574

Copyright terms: Public domain