This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. CH
chjcl.2 
|- B e. CH
Assertion chlejb1i 
|- ( A C_ B <-> ( A vH B ) = B )

Proof

Step Hyp Ref Expression
1 ch0le.1 
 |-  A e. CH
2 chjcl.2 
 |-  B e. CH
3 ssid 
 |-  B C_ B
4 1 2 2 chlubii 
 |-  ( ( A C_ B /\ B C_ B ) -> ( A vH B ) C_ B )
5 3 4 mpan2 
 |-  ( A C_ B -> ( A vH B ) C_ B )
6 2 1 chub2i 
 |-  B C_ ( A vH B )
7 5 6 jctir 
 |-  ( A C_ B -> ( ( A vH B ) C_ B /\ B C_ ( A vH B ) ) )
8 eqss 
 |-  ( ( A vH B ) = B <-> ( ( A vH B ) C_ B /\ B C_ ( A vH B ) ) )
9 7 8 sylibr 
 |-  ( A C_ B -> ( A vH B ) = B )
10 1 2 chub1i 
 |-  A C_ ( A vH B )
11 eqimss 
 |-  ( ( A vH B ) = B -> ( A vH B ) C_ B )
12 10 11 sstrid 
 |-  ( ( A vH B ) = B -> A C_ B )
13 9 12 impbii 
 |-  ( A C_ B <-> ( A vH B ) = B )