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	⊢ ∨ℋ = ( 𝑥 ∈ 𝒫 ℋ , 𝑦 ∈ 𝒫 ℋ ↦ ( ⊥ ‘ ( ⊥ ‘ ( 𝑥 ∪ 𝑦 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chj	⊢ ∨ℋ
1		vx	⊢ 𝑥
2		chba	⊢ ℋ
3	2	cpw	⊢ 𝒫 ℋ
4		vy	⊢ 𝑦
5		cort	⊢ ⊥
6	1	cv	⊢ 𝑥
7	4	cv	⊢ 𝑦
8	6 7	cun	⊢ ( 𝑥 ∪ 𝑦 )
9	8 5	cfv	⊢ ( ⊥ ‘ ( 𝑥 ∪ 𝑦 ) )
10	9 5	cfv	⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝑥 ∪ 𝑦 ) ) )
11	1 4 3 3 10	cmpo	⊢ ( 𝑥 ∈ 𝒫 ℋ , 𝑦 ∈ 𝒫 ℋ ↦ ( ⊥ ‘ ( ⊥ ‘ ( 𝑥 ∪ 𝑦 ) ) ) )
12	0 11	wceq	⊢ ∨ℋ = ( 𝑥 ∈ 𝒫 ℋ , 𝑦 ∈ 𝒫 ℋ ↦ ( ⊥ ‘ ( ⊥ ‘ ( 𝑥 ∪ 𝑦 ) ) ) )