Definition df-chj 9213

Description: Define Hilbert lattice join. See chjvalt 9260 for its value and chjclt 9267 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 9265. For an alternate definition see dfchj2 9262.

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 953	. . . . . 6 class x
4		chil 8727	. . . . . 6 class ℋ
5	3, 4	wss 2043	. . . . 5 wff x ⊆ ℋ
6		vy	. . . . . . 7 set y
7	6	cv 953	. . . . . 6 class y
8	7, 4	wss 2043	. . . . 5 wff y ⊆ ℋ
9	5, 8	wa 223	. . . 4 wff (x ⊆ ℋ ⋀ y ⊆ ℋ )
10		vz	. . . . . 6 set z
11	10	cv 953	. . . . 5 class z
12	3, 7	cun 2041	. . . . . . 7 class (x ∪ y)
13		cort 8738	. . . . . . 7 class ⊥
14	12, 13	cfv 3177	. . . . . 6 class (⊥ ‘(x ∪ y))
15	14, 13	cfv 3177	. . . . 5 class (⊥ ‘(⊥ ‘(x ∪ y)))
16	11, 15	wceq 954	. . . 4 wff z = (⊥ ‘(⊥ ‘(x ∪ y)))
17	9, 16	wa 223	. . 3 wff ((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = (⊥ ‘(⊥ ‘(x ∪ y))))
18	17, 2, 6, 10	copab2 3955	. 2 class {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = (⊥ ‘(⊥ ‘(x ∪ y))))}
19	1, 18	wceq 954	1 wff ∨ℋ = {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = (⊥ ‘(⊥ ‘(x ∪ y))))}

This definition is referenced by:  sshjvalt 9258  dfchj2 9262  dfchj3 9263

Copyright terms: Public domain