Metamath Proof Explorer

Theorem ssjo

Description: The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion ssjo ⊢ A ⊆ ℋ → A ∨ ℋ ⊥ ⁡ A = ℋ

Proof

Step Hyp Ref Expression
1 ocss ⊢ A ⊆ ℋ → ⊥ ⁡ A ⊆ ℋ
2 sshjval ⊢ A ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ → A ∨ ℋ ⊥ ⁡ A = ⊥ ⁡ ⊥ ⁡ A ∪ ⊥ ⁡ A
3 1 2 mpdan ⊢ A ⊆ ℋ → A ∨ ℋ ⊥ ⁡ A = ⊥ ⁡ ⊥ ⁡ A ∪ ⊥ ⁡ A
4 ssun1 ⊢ A ⊆ A ∪ ⊥ ⁡ A
5 1 ancli ⊢ A ⊆ ℋ → A ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ
6 unss ⊢ A ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ ↔ A ∪ ⊥ ⁡ A ⊆ ℋ
7 5 6 sylib ⊢ A ⊆ ℋ → A ∪ ⊥ ⁡ A ⊆ ℋ
8 occon ⊢ A ⊆ ℋ ∧ A ∪ ⊥ ⁡ A ⊆ ℋ → A ⊆ A ∪ ⊥ ⁡ A → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ A
9 7 8 mpdan ⊢ A ⊆ ℋ → A ⊆ A ∪ ⊥ ⁡ A → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ A
10 4 9 mpi ⊢ A ⊆ ℋ → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ A
11 ssun2 ⊢ ⊥ ⁡ A ⊆ A ∪ ⊥ ⁡ A
12 occon ⊢ ⊥ ⁡ A ⊆ ℋ ∧ A ∪ ⊥ ⁡ A ⊆ ℋ → ⊥ ⁡ A ⊆ A ∪ ⊥ ⁡ A → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A
13 1 7 12 syl2anc ⊢ A ⊆ ℋ → ⊥ ⁡ A ⊆ A ∪ ⊥ ⁡ A → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A
14 11 13 mpi ⊢ A ⊆ ℋ → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ A
15 10 14 ssind ⊢ A ⊆ ℋ → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A
16 ocsh ⊢ A ⊆ ℋ → ⊥ ⁡ A ∈ S ℋ
17 ocin ⊢ ⊥ ⁡ A ∈ S ℋ → ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A = 0 ℋ
18 16 17 syl ⊢ A ⊆ ℋ → ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A = 0 ℋ
19 15 18 sseqtrd ⊢ A ⊆ ℋ → ⊥ ⁡ A ∪ ⊥ ⁡ A ⊆ 0 ℋ
20 ocsh ⊢ A ∪ ⊥ ⁡ A ⊆ ℋ → ⊥ ⁡ A ∪ ⊥ ⁡ A ∈ S ℋ
21 sh0le ⊢ ⊥ ⁡ A ∪ ⊥ ⁡ A ∈ S ℋ → 0 ℋ ⊆ ⊥ ⁡ A ∪ ⊥ ⁡ A
22 7 20 21 3syl ⊢ A ⊆ ℋ → 0 ℋ ⊆ ⊥ ⁡ A ∪ ⊥ ⁡ A
23 19 22 eqssd ⊢ A ⊆ ℋ → ⊥ ⁡ A ∪ ⊥ ⁡ A = 0 ℋ
24 23 fveq2d ⊢ A ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ A ∪ ⊥ ⁡ A = ⊥ ⁡ 0 ℋ
25 choc0 ⊢ ⊥ ⁡ 0 ℋ = ℋ
26 24 25 eqtrdi ⊢ A ⊆ ℋ → ⊥ ⁡ ⊥ ⁡ A ∪ ⊥ ⁡ A = ℋ
27 3 26 eqtrd ⊢ A ⊆ ℋ → A ∨ ℋ ⊥ ⁡ A = ℋ