Metamath Proof Explorer

Theorem shlej1

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

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ⊆ B
2 unss1 ⊢ A ⊆ B → A ∪ C ⊆ B ∪ C
3 simpl1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∈ S ℋ
4 shss ⊢ A ∈ S ℋ → A ⊆ ℋ
5 3 4 syl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ⊆ ℋ
6 simpl3 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → C ∈ S ℋ
7 shss ⊢ C ∈ S ℋ → C ⊆ ℋ
8 6 7 syl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → C ⊆ ℋ
9 5 8 unssd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∪ C ⊆ ℋ
10 simpl2 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → B ∈ S ℋ
11 shss ⊢ B ∈ S ℋ → B ⊆ ℋ
12 10 11 syl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → B ⊆ ℋ
13 12 8 unssd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → B ∪ C ⊆ ℋ
14 occon2 ⊢ A ∪ C ⊆ ℋ ∧ B ∪ C ⊆ ℋ → A ∪ C ⊆ B ∪ C → ⊥ ⁡ ⊥ ⁡ A ∪ C ⊆ ⊥ ⁡ ⊥ ⁡ B ∪ C
15 9 13 14 syl2anc ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∪ C ⊆ B ∪ C → ⊥ ⁡ ⊥ ⁡ A ∪ C ⊆ ⊥ ⁡ ⊥ ⁡ B ∪ C
16 2 15 syl5 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ⊆ B → ⊥ ⁡ ⊥ ⁡ A ∪ C ⊆ ⊥ ⁡ ⊥ ⁡ B ∪ C
17 1 16 mpd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → ⊥ ⁡ ⊥ ⁡ A ∪ C ⊆ ⊥ ⁡ ⊥ ⁡ B ∪ C
18 shjval ⊢ A ∈ S ℋ ∧ C ∈ S ℋ → A ∨ ℋ C = ⊥ ⁡ ⊥ ⁡ A ∪ C
19 3 6 18 syl2anc ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∨ ℋ C = ⊥ ⁡ ⊥ ⁡ A ∪ C
20 shjval ⊢ B ∈ S ℋ ∧ C ∈ S ℋ → B ∨ ℋ C = ⊥ ⁡ ⊥ ⁡ B ∪ C
21 10 6 20 syl2anc ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → B ∨ ℋ C = ⊥ ⁡ ⊥ ⁡ B ∪ C
22 17 19 21 3sstr4d ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∨ ℋ C ⊆ B ∨ ℋ C