# Metamath Proof Explorer

## Theorem chnlei

Description: Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion chnlei ${⊢}¬{B}\subseteq {A}↔{A}\subset {A}{\vee }_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 2 chub1i ${⊢}{A}\subseteq {A}{\vee }_{ℋ}{B}$
4 3 biantrur ${⊢}¬{A}={A}{\vee }_{ℋ}{B}↔\left({A}\subseteq {A}{\vee }_{ℋ}{B}\wedge ¬{A}={A}{\vee }_{ℋ}{B}\right)$
5 2 1 chlejb1i ${⊢}{B}\subseteq {A}↔{B}{\vee }_{ℋ}{A}={A}$
6 eqcom ${⊢}{B}{\vee }_{ℋ}{A}={A}↔{A}={B}{\vee }_{ℋ}{A}$
7 2 1 chjcomi ${⊢}{B}{\vee }_{ℋ}{A}={A}{\vee }_{ℋ}{B}$
8 7 eqeq2i ${⊢}{A}={B}{\vee }_{ℋ}{A}↔{A}={A}{\vee }_{ℋ}{B}$
9 5 6 8 3bitri ${⊢}{B}\subseteq {A}↔{A}={A}{\vee }_{ℋ}{B}$
10 9 notbii ${⊢}¬{B}\subseteq {A}↔¬{A}={A}{\vee }_{ℋ}{B}$
11 dfpss2 ${⊢}{A}\subset {A}{\vee }_{ℋ}{B}↔\left({A}\subseteq {A}{\vee }_{ℋ}{B}\wedge ¬{A}={A}{\vee }_{ℋ}{B}\right)$
12 4 10 11 3bitr4i ${⊢}¬{B}\subseteq {A}↔{A}\subset {A}{\vee }_{ℋ}{B}$