Definition df-chj 26963

Description: Define Hilbert lattice join. See chjval 27005 for its value and chjcl 27010 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 27008. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.)

Assertion

Ref	Expression
df-chj	|- vH = ( x e. ~P ~H , y e. ~P ~H |-> ( _|_ ` ( _|_ ` ( x u. y ) ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-chj

Step	Hyp	Ref	Expression
1		chj 26586	. 2 class vH
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		chil 26572	. . . 4 class ~H
5	4	cpw 3951	. . 3 class ~P ~H
6	2	cv 1443	. . . . . 6 class x
7	3	cv 1443	. . . . . 6 class y
8	6, 7	cun 3402	. . . . 5 class ( x u. y )
9		cort 26583	. . . . 5 class _|_
10	8, 9	cfv 5582	. . . 4 class ( _|_ ` ( x u. y ) )
11	10, 9	cfv 5582	. . 3 class ( _|_ ` ( _|_ ` ( x u. y ) ) )
12	2, 3, 5, 5, 11	cmpt2 6292	. 2 class ( x e. ~P ~H , y e. ~P ~H |-> ( _|_ ` ( _|_ ` ( x u. y ) ) ) )
13	1, 12	wceq 1444	1 wff vH = ( x e. ~P ~H , y e. ~P ~H |-> ( _|_ ` ( _|_ ` ( x u. y ) ) ) )

This definition is referenced by:  sshjval  27003