Metamath Proof Explorer

Theorem chrelati

Description: The Hilbert lattice is relatively atomic. Remark 2 of Kalmbach p. 149. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 ⊢ A ∈ C ℋ
chpssat.2 ⊢ B ∈ C ℋ
Assertion chrelati ⊢ A ⊂ B → ∃ x ∈ HAtoms A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ A ∈ C ℋ
2 chpssat.2 ⊢ B ∈ C ℋ
3 1 2 chpssati ⊢ A ⊂ B → ∃ x ∈ HAtoms x ⊆ B ∧ ¬ x ⊆ A
4 ancom ⊢ x ⊆ B ∧ ¬ x ⊆ A ↔ ¬ x ⊆ A ∧ x ⊆ B
5 pssss ⊢ A ⊂ B → A ⊆ B
6 atelch ⊢ x ∈ HAtoms → x ∈ C ℋ
7 chnle ⊢ A ∈ C ℋ ∧ x ∈ C ℋ → ¬ x ⊆ A ↔ A ⊂ A ∨ ℋ x
8 1 7 mpan ⊢ x ∈ C ℋ → ¬ x ⊆ A ↔ A ⊂ A ∨ ℋ x
9 8 adantl ⊢ A ⊆ B ∧ x ∈ C ℋ → ¬ x ⊆ A ↔ A ⊂ A ∨ ℋ x
10 ibar ⊢ A ⊆ B → x ⊆ B ↔ A ⊆ B ∧ x ⊆ B
11 chlub ⊢ A ∈ C ℋ ∧ x ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B ∧ x ⊆ B ↔ A ∨ ℋ x ⊆ B
12 1 2 11 mp3an13 ⊢ x ∈ C ℋ → A ⊆ B ∧ x ⊆ B ↔ A ∨ ℋ x ⊆ B
13 10 12 sylan9bb ⊢ A ⊆ B ∧ x ∈ C ℋ → x ⊆ B ↔ A ∨ ℋ x ⊆ B
14 9 13 anbi12d ⊢ A ⊆ B ∧ x ∈ C ℋ → ¬ x ⊆ A ∧ x ⊆ B ↔ A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B
15 5 6 14 syl2an ⊢ A ⊂ B ∧ x ∈ HAtoms → ¬ x ⊆ A ∧ x ⊆ B ↔ A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B
16 4 15 bitrid ⊢ A ⊂ B ∧ x ∈ HAtoms → x ⊆ B ∧ ¬ x ⊆ A ↔ A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B
17 16 rexbidva ⊢ A ⊂ B → ∃ x ∈ HAtoms x ⊆ B ∧ ¬ x ⊆ A ↔ ∃ x ∈ HAtoms A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B
18 3 17 mpbid ⊢ A ⊂ B → ∃ x ∈ HAtoms A ⊂ A ∨ ℋ x ∧ A ∨ ℋ x ⊆ B