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

Metamath Proof Explorer

Theorem sshjval

Description: Value of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sshjval ⊢ 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 uneq12 ⊢ x = A ∧ y = B → x ∪ y = A ∪ B
5 4 fveq2d ⊢ x = A ∧ y = B → ⊥ ⁡ x ∪ y = ⊥ ⁡ A ∪ B
6 5 fveq2d ⊢ x = A ∧ y = B → ⊥ ⁡ ⊥ ⁡ x ∪ y = ⊥ ⁡ ⊥ ⁡ A ∪ B
7 df-chj ⊢ ∨ ℋ = x ∈ 𝒫 ℋ , y ∈ 𝒫 ℋ ⟼ ⊥ ⁡ ⊥ ⁡ x ∪ y
8 fvex ⊢ ⊥ ⁡ ⊥ ⁡ A ∪ B ∈ V
9 6 7 8 ovmpoa ⊢ A ∈ 𝒫 ℋ ∧ B ∈ 𝒫 ℋ → A ∨ ℋ B = ⊥ ⁡ ⊥ ⁡ A ∪ B
10 2 3 9 syl2anbr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ∨ ℋ B = ⊥ ⁡ ⊥ ⁡ A ∪ B