# Metamath Proof Explorer

## Theorem chabs2

Description: Hilbert lattice absorption law. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 16-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chabs2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap \left({A}{\vee }_{ℋ}{B}\right)={A}$

### Proof

Step Hyp Ref Expression
1 chub1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {A}{\vee }_{ℋ}{B}$
2 ssid ${⊢}{A}\subseteq {A}$
3 1 2 jctil ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {A}\wedge {A}\subseteq {A}{\vee }_{ℋ}{B}\right)$
4 ssin ${⊢}\left({A}\subseteq {A}\wedge {A}\subseteq {A}{\vee }_{ℋ}{B}\right)↔{A}\subseteq {A}\cap \left({A}{\vee }_{ℋ}{B}\right)$
5 3 4 sylib ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {A}\cap \left({A}{\vee }_{ℋ}{B}\right)$
6 inss1 ${⊢}{A}\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq {A}$
7 5 6 jctil ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq {A}\wedge {A}\subseteq {A}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
8 eqss ${⊢}{A}\cap \left({A}{\vee }_{ℋ}{B}\right)={A}↔\left({A}\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq {A}\wedge {A}\subseteq {A}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
9 7 8 sylibr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap \left({A}{\vee }_{ℋ}{B}\right)={A}$