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
|- ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )

Proof

Step Hyp Ref Expression
1 sseq2
 |-  ( A = if ( A e. CH , A , 0H ) -> ( B C_ A <-> B C_ if ( A e. CH , A , 0H ) ) )
2 1 notbid
 |-  ( A = if ( A e. CH , A , 0H ) -> ( -. B C_ A <-> -. B C_ if ( A e. CH , A , 0H ) ) )
3 id
 |-  ( A = if ( A e. CH , A , 0H ) -> A = if ( A e. CH , A , 0H ) )
4 oveq1
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A vH B ) = ( if ( A e. CH , A , 0H ) vH B ) )
5 3 4 psseq12d
 |-  ( A = if ( A e. CH , A , 0H ) -> ( A C. ( A vH B ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) )
6 2 5 bibi12d
 |-  ( A = if ( A e. CH , A , 0H ) -> ( ( -. B C_ A <-> A C. ( A vH B ) ) <-> ( -. B C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) ) )
7 sseq1
 |-  ( B = if ( B e. CH , B , 0H ) -> ( B C_ if ( A e. CH , A , 0H ) <-> if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) ) )
8 7 notbid
 |-  ( B = if ( B e. CH , B , 0H ) -> ( -. B C_ if ( A e. CH , A , 0H ) <-> -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) ) )
9 oveq2
 |-  ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) vH B ) = ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) )
10 9 psseq2d
 |-  ( B = if ( B e. CH , B , 0H ) -> ( if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) )
11 8 10 bibi12d
 |-  ( B = if ( B e. CH , B , 0H ) -> ( ( -. B C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH B ) ) <-> ( -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) ) ) )
12 h0elch
 |-  0H e. CH
13 12 elimel
 |-  if ( A e. CH , A , 0H ) e. CH
14 12 elimel
 |-  if ( B e. CH , B , 0H ) e. CH
15 13 14 chnlei
 |-  ( -. if ( B e. CH , B , 0H ) C_ if ( A e. CH , A , 0H ) <-> if ( A e. CH , A , 0H ) C. ( if ( A e. CH , A , 0H ) vH if ( B e. CH , B , 0H ) ) )
16 6 11 15 dedth2h
 |-  ( ( A e. CH /\ B e. CH ) -> ( -. B C_ A <-> A C. ( A vH B ) ) )