Definition df-chsup 9231

Description: Define the supremum of a set of Hilbert lattice elements. See chsupval2t 9257 for its value and dfchsup2 9253 for an alternate definition. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice C_ℋ, to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupclt 9262.

Assertion

Ref	Expression
df-chsup	⊢ ∨ℋ = {⟨x, y⟩∣(x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-chsup

Step	Hyp	Ref	Expression
1		chsup 8758	. 2 class ∨ℋ
2		vx	. . . . . 6 set x
3	2	cv 954	. . . . 5 class x
4		chil 8743	. . . . . 6 class ℋ
5	4	cpw 2398	. . . . 5 class ℘ ℋ
6	3, 5	wss 2044	. . . 4 wff x ⊆ ℘ ℋ
7		vy	. . . . . 6 set y
8	7	cv 954	. . . . 5 class y
9	3	cuni 2499	. . . . . . 7 class ∪x
10		cort 8754	. . . . . . 7 class ⊥
11	9, 10	cfv 3178	. . . . . 6 class (⊥ ‘∪x)
12	11, 10	cfv 3178	. . . . 5 class (⊥ ‘(⊥ ‘∪x))
13	8, 12	wceq 955	. . . 4 wff y = (⊥ ‘(⊥ ‘∪x))
14	6, 13	wa 223	. . 3 wff (x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))
15	14, 2, 7	copab 2662	. 2 class {⟨x, y⟩∣(x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))}
16	1, 15	wceq 955	1 wff ∨ℋ = {⟨x, y⟩∣(x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))}

This definition is referenced by:  dfchsup2 9253

Copyright terms: Public domain