Definition df-chsup 5278

Description: Define the supremum of a set of Hilbert lattice elements. See chsupval2t 5303 for its value and dfchsup2 5299 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 hsupclt 5308.

Assertion

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

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-chsup

Step	Hyp	Ref	Expression
1		chsup 4973	. 2 class \/H
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		chil 4958	. . . . . 6 class H~
5	4	cpw 1798	. . . . 5 class P~H~
6	3, 5	wss 1487	. . . 4 wff x (_ P~H~
7		vy	. . . . . 6 set y
8	7	cv 1089	. . . . 5 class y
9	3	cuni 1919	. . . . . . 7 class U.x
10		cort 4969	. . . . . . 7 class _|_
11	9, 10	cfv 2422	. . . . . 6 class (_|_` U.x)
12	11, 10	cfv 2422	. . . . 5 class (_|_` (_|_` U.x))
13	8, 12	wceq 1091	. . . 4 wff y = (_|_` (_|_` U.x))
14	6, 13	wa 196	. . 3 wff (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))
15	14, 2, 7	copab 2055	. 2 class {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}
16	1, 15	wceq 1091	1 wff \/H = {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}

This definition is referenced by:  dfchsup2 5299

metamath.org