# Metamath Proof Explorer

## Theorem chlejb1i

Description: Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 ssid ${⊢}{B}\subseteq {B}$
4 1 2 2 chlubii ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {B}\right)\to {A}{\vee }_{ℋ}{B}\subseteq {B}$
5 3 4 mpan2 ${⊢}{A}\subseteq {B}\to {A}{\vee }_{ℋ}{B}\subseteq {B}$
6 2 1 chub2i ${⊢}{B}\subseteq {A}{\vee }_{ℋ}{B}$
7 5 6 jctir ${⊢}{A}\subseteq {B}\to \left({A}{\vee }_{ℋ}{B}\subseteq {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}{B}\right)$
8 eqss ${⊢}{A}{\vee }_{ℋ}{B}={B}↔\left({A}{\vee }_{ℋ}{B}\subseteq {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}{B}\right)$
9 7 8 sylibr ${⊢}{A}\subseteq {B}\to {A}{\vee }_{ℋ}{B}={B}$
10 1 2 chub1i ${⊢}{A}\subseteq {A}{\vee }_{ℋ}{B}$
11 eqimss ${⊢}{A}{\vee }_{ℋ}{B}={B}\to {A}{\vee }_{ℋ}{B}\subseteq {B}$
12 10 11 sstrid ${⊢}{A}{\vee }_{ℋ}{B}={B}\to {A}\subseteq {B}$
13 9 12 impbii ${⊢}{A}\subseteq {B}↔{A}{\vee }_{ℋ}{B}={B}$