This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-chj

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 chj 
 |-  vH
1 vx 
 |-  x
2 chba 
 |-  ~H
3 2 cpw 
 |-  ~P ~H
4 vy 
 |-  y
5 cort 
 |-  _|_
6 1 cv 
 |-  x
7 4 cv 
 |-  y
8 6 7 cun 
 |-  ( x u. y )
9 8 5 cfv 
 |-  ( _|_ ` ( x u. y ) )
10 9 5 cfv 
 |-  ( _|_ ` ( _|_ ` ( x u. y ) ) )
11 1 4 3 3 10 cmpo 
 |-  ( x e. ~P ~H , y e. ~P ~H |-> ( _|_ ` ( _|_ ` ( x u. y ) ) ) )
12 0 11 wceq 
 |-  vH = ( x e. ~P ~H , y e. ~P ~H |-> ( _|_ ` ( _|_ ` ( x u. y ) ) ) )