Definition df-chj 9190

Description: Define Hilbert lattice join. See chjvalt 9237 for its value and chjclt 9244 for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to C_ℋ; see sshjclt 9242. For an alternate definition see dfchj2 9239.

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-chj

Step	Hyp	Ref	Expression
1		chj 8741	. 2 class ∨ℋ
2		vx	. . . . . . 7 set x
3	2	cv 952	. . . . . 6 class x
4		chil 8727	. . . . . 6 class ℋ
5	3, 4	wss 2037	. . . . 5 wff x ⊆ ℋ
6		vy	. . . . . . 7 set y
7	6	cv 952	. . . . . 6 class y
8	7, 4	wss 2037	. . . . 5 wff y ⊆ ℋ
9	5, 8	wa 223	. . . 4 wff (x ⊆ ℋ ⋀ y ⊆ ℋ )
10		vz	. . . . . 6 set z
11	10	cv 952	. . . . 5 class z
12	3, 7	cun 2035	. . . . . . 7 class (x ∪ y)
13		cort 8738	. . . . . . 7 class ⊥
14	12, 13	cfv 3172	. . . . . 6 class (⊥ ‘(x ∪ y))
15	14, 13	cfv 3172	. . . . 5 class (⊥ ‘(⊥ ‘(x ∪ y)))
16	11, 15	wceq 953	. . . 4 wff z = (⊥ ‘(⊥ ‘(x ∪ y)))
17	9, 16	wa 223	. . 3 wff ((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = (⊥ ‘(⊥ ‘(x ∪ y))))
18	17, 2, 6, 10	copab2 3949	. 2 class {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = (⊥ ‘(⊥ ‘(x ∪ y))))}
19	1, 18	wceq 953	1 wff ∨ℋ = {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = (⊥ ‘(⊥ ‘(x ∪ y))))}

This definition is referenced by:  sshjvalt 9235  dfchj2 9239  dfchj3 9240

Copyright terms: Public domain