Definition df-chj 9270

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

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 8797	. 2 class vH
2		vx	. . . . . . 7 set x
3	2	cv 957	. . . . . 6 class x
4		chil 8783	. . . . . 6 class H~
5	3, 4	wss 2050	. . . . 5 wff x (_ H~
6		vy	. . . . . . 7 set y
7	6	cv 957	. . . . . 6 class y
8	7, 4	wss 2050	. . . . 5 wff y (_ H~
9	5, 8	wa 223	. . . 4 wff (x (_ H~ /\ y (_ H~)
10		vz	. . . . . 6 set z
11	10	cv 957	. . . . 5 class z
12	3, 7	cun 2048	. . . . . . 7 class (x u. y)
13		cort 8794	. . . . . . 7 class _|_
14	12, 13	cfv 3188	. . . . . 6 class (_|_` (x u. y))
15	14, 13	cfv 3188	. . . . 5 class (_|_` (_|_` (x u. y)))
16	11, 15	wceq 958	. . . 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 3970	. 2 class {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}
19	1, 18	wceq 958	1 wff vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}

This definition is referenced by:  sshjvalt 9315  dfchj2 9319  dfchj3 9320

Copyright terms: Public domain