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

Metamath Proof Explorer

Theorem shlej2

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

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

Proof

Step Hyp Ref Expression
1 shlej1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∨ ℋ C ⊆ B ∨ ℋ C
2 shjcom ⊢ A ∈ S ℋ ∧ C ∈ S ℋ → A ∨ ℋ C = C ∨ ℋ A
3 2 3adant2 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ → A ∨ ℋ C = C ∨ ℋ A
4 3 adantr ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∨ ℋ C = C ∨ ℋ A
5 shjcom ⊢ B ∈ S ℋ ∧ C ∈ S ℋ → B ∨ ℋ C = C ∨ ℋ B
6 5 3adant1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ → B ∨ ℋ C = C ∨ ℋ B
7 6 adantr ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → B ∨ ℋ C = C ∨ ℋ B
8 1 4 7 3sstr3d ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → C ∨ ℋ A ⊆ C ∨ ℋ B