Definition df-chj 5277

Description: Define Hilbert lattice join. See chjvalt 5323 for its value and chjclt 5330 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 5328. For an alternate definition see dfchj2 5325.

Assertion

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

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-chj

Step	Hyp	Ref	Expression
1		chj 4972	. 2 class ∨ℋ
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		chil 4958	. . . . . 6 class ℋ
5	3, 4	wss 1487	. . . . 5 wff x ⊆ ℋ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wss 1487	. . . . 5 wff y ⊆ ℋ
9	5, 8	wa 196	. . . 4 wff (x ⊆ ℋ ∧ y ⊆ ℋ )
10		vz	. . . . . 6 set z
11	10	cv 1089	. . . . 5 class z
12	3, 7	cun 1485	. . . . . . 7 class (x ∪ y)
13		cort 4969	. . . . . . 7 class ⊥
14	12, 13	cfv 2422	. . . . . 6 class (⊥ ‘(x ∪ y))
15	14, 13	cfv 2422	. . . . 5 class (⊥ ‘(⊥ ‘(x ∪ y)))
16	11, 15	wceq 1091	. . . 4 wff z = (⊥ ‘(⊥ ‘(x ∪ y)))
17	9, 16	wa 196	. . 3 wff ((x ⊆ ℋ ∧ y ⊆ ℋ ) ∧ z = (⊥ ‘(⊥ ‘(x ∪ y))))
18	17, 2, 6, 10	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ∧ y ⊆ ℋ ) ∧ z = (⊥ ‘(⊥ ‘(x ∪ y))))}
19	1, 18	wceq 1091	1 wff ∨ℋ = {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ∧ y ⊆ ℋ ) ∧ z = (⊥ ‘(⊥ ‘(x ∪ y))))}

This definition is referenced by:  sshjvalt 5321  dfchj2 5325  dfchj3 5326

metamath.org