# Metamath Proof Explorer

## Theorem chnle

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

Ref Expression
Assertion chnle ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(¬{B}\subseteq {A}↔{A}\subset {A}{\vee }_{ℋ}{B}\right)$

### Proof

Step Hyp Ref Expression
1 sseq2 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({B}\subseteq {A}↔{B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)$
2 1 notbid ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left(¬{B}\subseteq {A}↔¬{B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)$
3 id ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to {A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)$
4 oveq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to {A}{\vee }_{ℋ}{B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}$
5 3 4 psseq12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({A}\subset {A}{\vee }_{ℋ}{B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}\right)$
6 2 5 bibi12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left(\left(¬{B}\subseteq {A}↔{A}\subset {A}{\vee }_{ℋ}{B}\right)↔\left(¬{B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}\right)\right)$
7 sseq1 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left({B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)↔if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)$
8 7 notbid ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(¬{B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)↔¬if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)$
9 oveq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
10 9 psseq2d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)$
11 8 10 bibi12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(\left(¬{B}\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}\right)↔\left(¬if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)\right)$
12 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
13 12 elimel ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
14 12 elimel ${⊢}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
15 13 14 chnlei ${⊢}¬if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\subseteq if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subset if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
16 6 11 15 dedth2h ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(¬{B}\subseteq {A}↔{A}\subset {A}{\vee }_{ℋ}{B}\right)$