Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-chj | Structured version Visualization version GIF version |
Description: Define Hilbert lattice join. See chjval 27595 for its value and chjcl 27600 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 Cℋ; see sshjcl 27598. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-chj | ⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chj 27174 | . 2 class ∨ℋ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | chil 27160 | . . . 4 class ℋ | |
5 | 4 | cpw 4108 | . . 3 class 𝒫 ℋ |
6 | 2 | cv 1474 | . . . . . 6 class 𝑥 |
7 | 3 | cv 1474 | . . . . . 6 class 𝑦 |
8 | 6, 7 | cun 3538 | . . . . 5 class (𝑥 ∪ 𝑦) |
9 | cort 27171 | . . . . 5 class ⊥ | |
10 | 8, 9 | cfv 5804 | . . . 4 class (⊥‘(𝑥 ∪ 𝑦)) |
11 | 10, 9 | cfv 5804 | . . 3 class (⊥‘(⊥‘(𝑥 ∪ 𝑦))) |
12 | 2, 3, 5, 5, 11 | cmpt2 6551 | . 2 class (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) |
13 | 1, 12 | wceq 1475 | 1 wff ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) |
Colors of variables: wff setvar class |
This definition is referenced by: sshjval 27593 |
Copyright terms: Public domain | W3C validator |