Metamath Proof Explorer

Theorem cvati

Description: If a Hilbert lattice element covers another, it equals the other joined with some atom. This is a consequence of the relative atomicity of Hilbert space. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 ⊢ A ∈ C ℋ
chpssat.2 ⊢ B ∈ C ℋ
Assertion cvati ⊢ A ⋖ ℋ B → ∃ x ∈ HAtoms A ∨ ℋ x = B

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ A ∈ C ℋ
2 chpssat.2 ⊢ B ∈ C ℋ
3 cvpss ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B → A ⊂ B
4 1 2 3 mp2an ⊢ A ⋖ ℋ B → A ⊂ B
5 1 2 chrelati ⊢ A ⊂ B → ∃ x ∈ HAtoms A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B
6 4 5 syl ⊢ A ⋖ ℋ B → ∃ x ∈ HAtoms A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B
7 cvnbtwn2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ∨ ℋ x ∈ C ℋ → A ⋖ ℋ B → A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B → A ∨ ℋ x = B
8 1 2 7 mp3an12 ⊢ A ∨ ℋ x ∈ C ℋ → A ⋖ ℋ B → A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B → A ∨ ℋ x = B
9 atelch ⊢ x ∈ HAtoms → x ∈ C ℋ
10 chjcl ⊢ A ∈ C ℋ ∧ x ∈ C ℋ → A ∨ ℋ x ∈ C ℋ
11 1 9 10 sylancr ⊢ x ∈ HAtoms → A ∨ ℋ x ∈ C ℋ
12 8 11 syl11 ⊢ A ⋖ ℋ B → x ∈ HAtoms → A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B → A ∨ ℋ x = B
13 12 reximdvai ⊢ A ⋖ ℋ B → ∃ x ∈ HAtoms A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B → ∃ x ∈ HAtoms A ∨ ℋ x = B
14 6 13 mpd ⊢ A ⋖ ℋ B → ∃ x ∈ HAtoms A ∨ ℋ x = B