Definition df-chj 9275

Description: Define Hilbert lattice join. See chjvalt 9322 for its value and chjclt 9329 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 sshjclt 9327. For an alternate definition see dfchj2 9324.

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 8802	. 2 class vH
2		vx	. . . . . . 7 set x
3	2	cv 955	. . . . . 6 class x
4		chil 8788	. . . . . 6 class H~
5	3, 4	wss 2047	. . . . 5 wff x (_ H~
6		vy	. . . . . . 7 set y
7	6	cv 955	. . . . . 6 class y
8	7, 4	wss 2047	. . . . 5 wff y (_ H~
9	5, 8	wa 223	. . . 4 wff (x (_ H~ /\ y (_ H~)
10		vz	. . . . . 6 set z
11	10	cv 955	. . . . 5 class z
12	3, 7	cun 2045	. . . . . . 7 class (x u. y)
13		cort 8799	. . . . . . 7 class _|_
14	12, 13	cfv 3182	. . . . . 6 class (_|_` (x u. y))
15	14, 13	cfv 3182	. . . . 5 class (_|_` (_|_` (x u. y)))
16	11, 15	wceq 956	. . . 4 wff z = (_|_` (_|_` (x u. y)))
17	9, 16	wa 223	. . 3 wff ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))
18	17, 2, 6, 10	copab2 3964	. 2 class {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}
19	1, 18	wceq 956	1 wff vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}

This definition is referenced by:  sshjvalt 9320  dfchj2 9324  dfchj3 9325

Copyright terms: Public domain