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 30071 for its value and chjcl 30076 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 30074. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-chj | ⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chj 29652 | . 2 class ∨ℋ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | vy | . . 3 setvar 𝑦 | |
4 | chba 29638 | . . . 4 class ℋ | |
5 | 4 | cpw 4558 | . . 3 class 𝒫 ℋ |
6 | 2 | cv 1540 | . . . . . 6 class 𝑥 |
7 | 3 | cv 1540 | . . . . . 6 class 𝑦 |
8 | 6, 7 | cun 3906 | . . . . 5 class (𝑥 ∪ 𝑦) |
9 | cort 29649 | . . . . 5 class ⊥ | |
10 | 8, 9 | cfv 6491 | . . . 4 class (⊥‘(𝑥 ∪ 𝑦)) |
11 | 10, 9 | cfv 6491 | . . 3 class (⊥‘(⊥‘(𝑥 ∪ 𝑦))) |
12 | 2, 3, 5, 5, 11 | cmpo 7351 | . 2 class (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) |
13 | 1, 12 | wceq 1541 | 1 wff ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) |
Colors of variables: wff setvar class |
This definition is referenced by: sshjval 30069 |
Copyright terms: Public domain | W3C validator |