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

Metamath Proof Explorer

Theorem shub2

Description: A subspace is a subset of its Hilbert lattice join with another. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shub2 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ B ∨ ℋ A

Proof

Step Hyp Ref Expression
1 shub1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ A ∨ ℋ B
2 shjcom ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ∨ ℋ B = B ∨ ℋ A
3 1 2 sseqtrd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ B ∨ ℋ A