# Metamath Proof Explorer

## Theorem chlejb1

Description: Hilbert lattice ordering in terms of join. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 sseq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({A}\subseteq {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}\right)$
2 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}$
3 2 eqeq1d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({A}{\vee }_{ℋ}{B}={B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}={B}\right)$
4 1 3 bibi12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left(\left({A}\subseteq {B}↔{A}{\vee }_{ℋ}{B}={B}\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}={B}\right)\right)$
5 sseq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)$
6 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)$
7 id ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to {B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
8 6 7 eqeq12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}={B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)$
9 5 8 bibi12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}{B}={B}\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)\right)$
10 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
11 10 elimel ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
12 10 elimel ${⊢}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
13 11 12 chlejb1i ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
14 4 9 13 dedth2h ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}↔{A}{\vee }_{ℋ}{B}={B}\right)$