Definition df-chsup 9278

Description: Define the supremum of a set of Hilbert lattice elements. See chsupval2t 9304 for its value and dfchsup2 9300 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 9309.

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 8805	. 2 class \/H
2		vx	. . . . . 6 set x
3	2	cv 957	. . . . 5 class x
4		chil 8790	. . . . . 6 class H~
5	4	cpw 2406	. . . . 5 class P~H~
6	3, 5	wss 2051	. . . 4 wff x (_ P~H~
7		vy	. . . . . 6 set y
8	7	cv 957	. . . . 5 class y
9	3	cuni 2508	. . . . . . 7 class U.x
10		cort 8801	. . . . . . 7 class _|_
11	9, 10	cfv 3189	. . . . . 6 class (_|_` U.x)
12	11, 10	cfv 3189	. . . . 5 class (_|_` (_|_` U.x))
13	8, 12	wceq 958	. . . 4 wff y = (_|_` (_|_` U.x))
14	6, 13	wa 223	. . 3 wff (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))
15	14, 2, 7	copab 2672	. 2 class {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}
16	1, 15	wceq 958	1 wff \/H = {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}

This definition is referenced by:  dfchsup2 9300

Copyright terms: Public domain