Metamath Proof Explorer

Theorem sshjval3

Description: Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in Beran p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice CH . (Contributed by NM, 2-Mar-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sshjval3 ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ∨ ℋ B = ⋁ ℋ ⁡ A B

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 elpw2 ⊢ A ∈ 𝒫 ℋ ↔ A ⊆ ℋ
3 1 elpw2 ⊢ B ∈ 𝒫 ℋ ↔ B ⊆ ℋ
4 uniprg ⊢ A ∈ 𝒫 ℋ ∧ B ∈ 𝒫 ℋ → ⋃ A B = A ∪ B
5 2 3 4 syl2anbr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → ⋃ A B = A ∪ B
6 5 fveq2d ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → ⊥ ⁡ ⋃ A B = ⊥ ⁡ A ∪ B
7 6 fveq2d ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ ⋃ A B = ⊥ ⁡ ⊥ ⁡ A ∪ B
8 prssi ⊢ A ∈ 𝒫 ℋ ∧ B ∈ 𝒫 ℋ → A B ⊆ 𝒫 ℋ
9 2 3 8 syl2anbr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A B ⊆ 𝒫 ℋ
10 hsupval ⊢ A B ⊆ 𝒫 ℋ → ⋁ ℋ ⁡ A B = ⊥ ⁡ ⊥ ⁡ ⋃ A B
11 9 10 syl ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → ⋁ ℋ ⁡ A B = ⊥ ⁡ ⊥ ⁡ ⋃ A B
12 sshjval ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ∨ ℋ B = ⊥ ⁡ ⊥ ⁡ A ∪ B
13 7 11 12 3eqtr4rd ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ∨ ℋ B = ⋁ ℋ ⁡ A B