Definition df-chj 10700

Description: Define Hilbert lattice join. See chjval 10747 for its value and chjcl 10754 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 CH; see sshjcl 10752. For an alternate definition see dfchj2 10749.

Assertion

Ref	Expression
df-chj	|- vH = {<.<.x, y>., z>. | ((x C_ ~H /\ y C_ ~H) /\ z = (_|_` (_|_` (x u. y))))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-chj

Step	Hyp	Ref	Expression
1		chj 10226	. 2 class vH
2		vx	. . . . . . 7 set x
3	2	cv 1135	. . . . . 6 class x
4		chil 10212	. . . . . 6 class ~H
5	3, 4	wss 2426	. . . . 5 wff x C_ ~H
6		vy	. . . . . . 7 set y
7	6	cv 1135	. . . . . 6 class y
8	7, 4	wss 2426	. . . . 5 wff y C_ ~H
9	5, 8	wa 239	. . . 4 wff (x C_ ~H /\ y C_ ~H)
10		vz	. . . . . 6 set z
11	10	cv 1135	. . . . 5 class z
12	3, 7	cun 2424	. . . . . . 7 class (x u. y)
13		cort 10223	. . . . . . 7 class _|_
14	12, 13	cfv 3809	. . . . . 6 class (_|_` (x u. y))
15	14, 13	cfv 3809	. . . . 5 class (_|_` (_|_` (x u. y)))
16	11, 15	wceq 1136	. . . 4 wff z = (_|_` (_|_` (x u. y)))
17	9, 16	wa 239	. . 3 wff ((x C_ ~H /\ y C_ ~H) /\ z = (_|_` (_|_` (x u. y))))
18	17, 2, 6, 10	copab2 4696	. 2 class {<.<.x, y>., z>. | ((x C_ ~H /\ y C_ ~H) /\ z = (_|_` (_|_` (x u. y))))}
19	1, 18	wceq 1136	1 wff vH = {<.<.x, y>., z>. | ((x C_ ~H /\ y C_ ~H) /\ z = (_|_` (_|_` (x u. y))))}

This definition is referenced by:  sshjval 10745  dfchj2 10749  dfchj3 10750

Copyright terms: Public domain