Definition df-chsup 9191

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

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 8742	. 2 class ∨ℋ
2		vx	. . . . . 6 set x
3	2	cv 952	. . . . 5 class x
4		chil 8727	. . . . . 6 class ℋ
5	4	cpw 2391	. . . . 5 class ℘ ℋ
6	3, 5	wss 2037	. . . 4 wff x ⊆ ℘ ℋ
7		vy	. . . . . 6 set y
8	7	cv 952	. . . . 5 class y
9	3	cuni 2493	. . . . . . 7 class ∪x
10		cort 8738	. . . . . . 7 class ⊥
11	9, 10	cfv 3172	. . . . . 6 class (⊥ ‘∪x)
12	11, 10	cfv 3172	. . . . 5 class (⊥ ‘(⊥ ‘∪x))
13	8, 12	wceq 953	. . . 4 wff y = (⊥ ‘(⊥ ‘∪x))
14	6, 13	wa 223	. . 3 wff (x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))
15	14, 2, 7	copab 2656	. 2 class {⟨x, y⟩∣(x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))}
16	1, 15	wceq 953	1 wff ∨ℋ = {⟨x, y⟩∣(x ⊆ ℘ ℋ ⋀ y = (⊥ ‘(⊥ ‘∪x)))}

This definition is referenced by:  dfchsup2 9213

Copyright terms: Public domain