Definition df-chsup 9405

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

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 8983	. 2 class \/H
2		vx	. . . . . 6 set x
3	2	cv 1098	. . . . 5 class x
4		chil 8968	. . . . . 6 class H~
5	4	cpw 2372	. . . . 5 class P~H~
6	3, 5	wss 2018	. . . 4 wff x (_ P~H~
7		vy	. . . . . 6 set y
8	7	cv 1098	. . . . 5 class y
9	3	cuni 2471	. . . . . . 7 class U.x
10		cort 8979	. . . . . . 7 class _|_
11	9, 10	cfv 3145	. . . . . 6 class (_|_` U.x)
12	11, 10	cfv 3145	. . . . 5 class (_|_` (_|_` U.x))
13	8, 12	wceq 1099	. . . 4 wff y = (_|_` (_|_` U.x))
14	6, 13	wa 223	. . 3 wff (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))
15	14, 2, 7	copab 2634	. 2 class {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}
16	1, 15	wceq 1099	1 wff \/H = {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}

This definition is referenced by:  dfchsup2 9427

Copyright terms: Public domain