Metamath Proof Explorer

Theorem chcv2

Description: The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chcv2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⊂ A ∨ ℋ B ↔ A ⋖ ℋ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 atelch ⊢ B ∈ HAtoms → B ∈ C ℋ
2 chnle ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ¬ B ⊆ A ↔ A ⊂ A ∨ ℋ B
3 1 2 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ⊂ A ∨ ℋ B
4 chcv1 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ⋖ ℋ A ∨ ℋ B
5 3 4 bitr3d ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⊂ A ∨ ℋ B ↔ A ⋖ ℋ A ∨ ℋ B