Definition df-chj 9551

Description: Define Hilbert lattice join. See chjval 9598 for its value and chjcl 9605 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 9603. For an alternate definition see dfchj2 9600.

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-chj

Step	Hyp	Ref	Expression
1		chj 9077	. 2 class vH
2		vx	. . . . . . 7 set x
3	2	cv 991	. . . . . 6 class x
4		chil 9063	. . . . . 6 class H~
5	3, 4	wss 2099	. . . . 5 wff x (_ H~
6		vy	. . . . . . 7 set y
7	6	cv 991	. . . . . 6 class y
8	7, 4	wss 2099	. . . . 5 wff y (_ H~
9	5, 8	wa 221	. . . 4 wff (x (_ H~ /\ y (_ H~)
10		vz	. . . . . 6 set z
11	10	cv 991	. . . . 5 class z
12	3, 7	cun 2097	. . . . . . 7 class (x u. y)
13		cort 9074	. . . . . . 7 class _|_
14	12, 13	cfv 3263	. . . . . 6 class (_|_` (x u. y))
15	14, 13	cfv 3263	. . . . 5 class (_|_` (_|_` (x u. y)))
16	11, 15	wceq 992	. . . 4 wff z = (_|_` (_|_` (x u. y)))
17	9, 16	wa 221	. . 3 wff ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))
18	17, 2, 6, 10	copab2 4022	. 2 class {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}
19	1, 18	wceq 992	1 wff vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}

This definition is referenced by:  sshjval 9596  dfchj2 9600  dfchj3 9601

Copyright terms: Public domain