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

Metamath Proof Explorer

Theorem chlej1

Description: Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chlej1 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ A ⊆ B → A ∨ ℋ C ⊆ B ∨ ℋ C

Proof

Step Hyp Ref Expression
1 chsh ⊢ A ∈ C ℋ → A ∈ S ℋ
2 chsh ⊢ B ∈ C ℋ → B ∈ S ℋ
3 chsh ⊢ C ∈ C ℋ → C ∈ S ℋ
4 shlej1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∨ ℋ C ⊆ B ∨ ℋ C
5 1 2 3 4 syl3anl ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ C ∈ C ℋ ∧ A ⊆ B → A ∨ ℋ C ⊆ B ∨ ℋ C