HomeHome Metamath Proof Explorer
Theorem List (p. 299 of 315)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21494)
  Hilbert Space Explorer  Hilbert Space Explorer
(21495-23017)
  Users' Mathboxes  Users' Mathboxes
(23018-31433)
 

Theorem List for Metamath Proof Explorer - 29801-29900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcdleme21g 29801 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) )  /\  ( ( z  e.  A  /\  -.  z  .<_  W )  /\  ( P  .\/  z )  =  ( S  .\/  z ) ) ) )  ->  N  =  O )
 
Theoremcdleme21h 29802* Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( E. z  e.  A  ( -.  z  .<_  W  /\  ( P 
 .\/  z )  =  ( S  .\/  z
 ) )  ->  N  =  O ) )
 
Theoremcdleme21i 29803* Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P 
 .\/  Q ) ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( R  .<_  ( P 
 .\/  Q )  /\  U  .<_  ( S  .\/  T ) ) ) ) 
 ->  ( E. r  e.  A  ( -.  r  .<_  W  /\  ( P 
 .\/  r )  =  ( Q  .\/  r
 ) )  ->  N  =  O ) )
 
Theoremcdleme21j 29804* Combine cdleme20 29792 and cdleme21i 29803 to eliminate  U 
.<_  ( S  .\/  T
) condition. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) )  /\  E. r  e.  A  ( -.  r  .<_  W  /\  ( P  .\/  r )  =  ( Q  .\/  r ) ) ) )  ->  N  =  O )
 
Theoremcdleme21 29805 Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115.  D,  F,  N,  Y,  G,  O represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. Combine cdleme18d 29763 and cdleme21j 29804 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( P  =/=  Q  /\  S  =/=  T ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P  .\/  Q ) ) ) ) 
 ->  N  =  O )
 
Theoremcdleme21k 29806 Eliminate  S  =/=  T condition in cdleme21 29805. (Contributed by NM, 26-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  D  =  ( ( R  .\/  S )  ./\  W )   &    |-  Y  =  ( ( R  .\/  T )  ./\  W )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  D ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  Y ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( R  e.  A  /\  -.  R  .<_  W )  /\  ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  ( P  =/=  Q  /\  ( -.  S  .<_  ( P  .\/  Q )  /\  -.  T  .<_  ( P  .\/  Q )  /\  R  .<_  ( P 
 .\/  Q ) ) ) )  ->  N  =  O )
 
Theoremcdleme22aa 29807 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t 
\/ v = p  \/ q implies v = u. (Contributed by NM, 2-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  V  .<_  W  /\  V  .<_  ( P  .\/  Q ) ) )  ->  V  =  U )
 
Theoremcdleme22a 29808 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t 
\/ v = p  \/ q implies v = u. (Contributed by NM, 30-Nov-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  T  e.  A )  /\  ( ( V  e.  A  /\  V  .<_  W ) 
 /\  P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q ) ) ) 
 ->  V  =  U )
 
Theoremcdleme22b 29809 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t  \/ v =/= p  \/ q and s  <_ p  \/ q implies  -. t  <_ p  \/ q. (Contributed by NM, 2-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  (
 ( T  .\/  V )  =/=  ( P  .\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) ) 
 ->  -.  T  .<_  ( P 
 .\/  Q ) )
 
Theoremcdleme22cN 29810 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t  \/ v =/= p  \/ q and s  <_ p  \/ q implies  -. v  <_ p  \/ q. (Contributed by NM, 3-Dec-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  T  e.  A  /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( ( P  =/=  Q  /\  S  =/=  T )  /\  ( S  .<_  ( T 
 .\/  V )  /\  S  .<_  ( P  .\/  Q ) )  /\  ( T 
 .\/  V )  =/=  ( P  .\/  Q ) ) )  ->  -.  V  .<_  ( P  .\/  Q )
 )
 
Theoremcdleme22d 29811 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( S  =/=  T  /\  S  .<_  ( T  .\/  V ) ) )  ->  V  =  ( ( S  .\/  T )  ./\  W ) )
 
Theoremcdleme22e 29812 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. (Contributed by NM, 6-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W ) 
 /\  ( P  =/=  Q 
 /\  ( T  .\/  V )  =  ( P 
 .\/  Q ) )  /\  ( z  e.  A  /\  -.  z  .<_  W ) ) )  ->  N  .<_  ( O  .\/  V ) )
 
Theoremcdleme22eALTN 29813 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( y  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  y )  ./\  W ) ) )   &    |-  G  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  y )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  z )  ./\  W ) ) )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H  /\  T  e.  A )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  P  =/=  Q )  /\  ( S  e.  A  /\  ( V  e.  A  /\  V  .<_  W  /\  ( T  .\/  V )  =  ( P  .\/  Q ) )  /\  (
 ( y  e.  A  /\  -.  y  .<_  W ) 
 /\  ( z  e.  A  /\  -.  z  .<_  W ) ) ) )  ->  N  .<_  ( O  .\/  V )
 )
 
Theoremcdleme22f 29814 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  N represent f(t), ft(s) respectively. If s  <_ t  \/ v, then ft(s)  <_ f(t)  \/ v. (Contributed by NM, 6-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  T )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( S  e.  A  /\  -.  S  .<_  W ) 
 /\  T  e.  A  /\  ( V  e.  A  /\  V  .<_  W ) ) 
 /\  ( S  =/=  T 
 /\  S  .<_  ( T 
 .\/  V ) ) ) 
 ->  N  .<_  ( F  .\/  V ) )
 
Theoremcdleme22f2 29815 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 29814 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. (Contributed by NM, 7-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( -.  S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P 
 .\/  Q )  /\  P  =/=  Q ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S  =/=  T  /\  S  .<_  ( T  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  F  .<_  ( N  .\/  V )
 )
 
Theoremcdleme22g 29816 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  G represent f(s), f(t) respectively. If s  <_ t  \/ v and  -. s  <_ p  \/ q, then f(s)  <_ f(t)  \/ v. (Contributed by NM, 6-Dec-2012.)
 |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  G  =  ( ( T  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  T )  ./\  W )
 ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( -.  T  .<_  ( P  .\/  Q )  /\  -.  S  .<_  ( P  .\/  Q )  /\  P  =/=  Q ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( S  =/=  T  /\  S  .<_  ( T  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  F  .<_  ( G  .\/  V )
 )
 
Theoremcdleme23a 29817 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( S  .\/  T )  ./\  ( X  ./\ 
 W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( S  =/=  T  /\  ( S  .\/  ( X  ./\  W ) )  =  X  /\  ( T  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  V  .<_  W )
 
Theoremcdleme23b 29818 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( S  .\/  T )  ./\  ( X  ./\ 
 W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( S  =/=  T  /\  ( S  .\/  ( X  ./\  W ) )  =  X  /\  ( T  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  V  e.  A )
 
Theoremcdleme23c 29819 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  V  =  ( ( S  .\/  T )  ./\  ( X  ./\ 
 W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) ) 
 /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( S  =/=  T  /\  ( S  .\/  ( X  ./\  W ) )  =  X  /\  ( T  .\/  ( X  ./\  W ) )  =  X ) ) 
 ->  S  .<_  ( T  .\/  V ) )
 
Theoremcdleme24 29820* Quantified version of cdleme21k 29806. (Contributed by NM, 26-Dec-2012.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   &    |-  G  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( R  .\/  t )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  A. s  e.  A  A. t  e.  A  ( ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) ) )  ->  N  =  O )
 )
 
Theoremcdleme25a 29821* Lemma for cdleme25b 29822. (Contributed by NM, 1-Jan-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  N  e.  B ) )
 
Theoremcdleme25b 29822* Transform cdleme24 29820. TODO get rid of $d's on  U,  N (Contributed by NM, 1-Jan-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E. u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )
 
Theoremcdleme25c 29823* Transform cdleme25b 29822. (Contributed by NM, 1-Jan-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E! u  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  ->  u  =  N ) )
 
Theoremcdleme25dN 29824* Transform cdleme25c 29823. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  E! u  e.  B  E. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  /\  u  =  N ) )
 
Theoremcdleme25cl 29825* Show closure of the unique element in cdleme25c 29823. (Contributed by NM, 2-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ( P  =/=  Q  /\  R  .<_  ( P  .\/  Q ) ) )  ->  I  e.  B )
 
Theoremcdleme25cv 29826* Change bound variables in cdleme25c 29823. (Contributed by NM, 2-Feb-2013.)
 |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( R  .\/  s )  ./\  W ) ) )   &    |-  G  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( R  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   =>    |-  I  =  E
 
Theoremcdleme26e 29827* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( ( P  =/=  Q  /\  S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P  .\/  Q )
 )  /\  ( ( T  .\/  V )  =  ( P  .\/  Q )  /\  -.  z  .<_  ( P  .\/  Q )
 )  /\  ( z  e.  A  /\  -.  z  .<_  W ) ) ) 
 ->  I  .<_  ( E 
 .\/  V ) )
 
Theoremcdleme26ee 29828* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( ( S  e.  A  /\  -.  S  .<_  W )  /\  ( T  e.  A  /\  -.  T  .<_  W ) 
 /\  ( V  e.  A  /\  V  .<_  W ) )  /\  ( ( P  =/=  Q  /\  S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P  .\/  Q )
 )  /\  ( T  .\/  V )  =  ( P  .\/  Q )
 ) )  ->  I  .<_  ( E  .\/  V ) )
 
Theoremcdleme26eALTN 29829* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( y  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  y )  ./\  W ) ) )   &    |-  G  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  y )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  z )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. y  e.  A  ( ( -.  y  .<_  W  /\  -.  y  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  E  =  ( iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( S  e.  A  /\  -.  S  .<_  W 
 /\  S  .<_  ( P 
 .\/  Q ) )  /\  ( T  e.  A  /\  -.  T  .<_  W  /\  T  .<_  ( P  .\/  Q ) ) )  /\  ( ( V  e.  A  /\  V  .<_  W  /\  ( T  .\/  V )  =  ( P  .\/  Q ) )  /\  (
 y  e.  A  /\  -.  y  .<_  W  /\  -.  y  .<_  ( P  .\/  Q ) )  /\  (
 z  e.  A  /\  -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) ) ) ) 
 ->  I  .<_  ( E 
 .\/  V ) )
 
Theoremcdleme26fALTN 29830* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  N represent f(t), ft(s) respectively. If t  <_ t  \/ v, then ft(s)  <_ f(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  S  .<_  ( P 
 .\/  Q ) )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  (
 ( -.  t  .<_  W 
 /\  -.  t  .<_  ( P  .\/  Q )
 )  /\  ( S  =/=  t  /\  S  .<_  ( t  .\/  V )
 )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  I  .<_  ( F  .\/  V ) )
 
Theoremcdleme26f 29831* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.  F,  N represent f(t), ft(s) respectively. If t  <_ t  \/ v, then ft(s)  <_ f(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ u  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  S  .<_  ( P 
 .\/  Q ) )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( S  e.  A  /\  -.  S  .<_  W ) )  /\  ( -.  t  .<_  ( P 
 .\/  Q )  /\  ( S  =/=  t  /\  S  .<_  ( t  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) ) 
 ->  I  .<_  ( F 
 .\/  V ) )
 
Theoremcdleme26f2ALTN 29832* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 29830 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  G  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  s )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  T  .<_  ( P 
 .\/  Q ) )  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  (
 ( -.  s  .<_  W 
 /\  -.  s  .<_  ( P  .\/  Q )
 )  /\  ( s  =/=  T  /\  s  .<_  ( T  .\/  V )
 )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  G  .<_  ( E  .\/  V ) )
 
Theoremcdleme26f2 29833* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 29830 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  G  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( G  .\/  ( ( T  .\/  s )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  -.  s  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  =/=  Q 
 /\  T  .<_  ( P 
 .\/  Q ) )  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( T  e.  A  /\  -.  T  .<_  W ) )  /\  ( -.  s  .<_  ( P 
 .\/  Q )  /\  (
 s  =/=  T  /\  s  .<_  ( T  .\/  V ) )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  G  .<_  ( E  .\/  V )
 )
 
Theoremcdleme27cl 29834* Part of proof of Lemma E in [Crawley] p. 113. Closure of  C. (Contributed by NM, 6-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  (
 ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  (
 ( s  e.  A  /\  -.  s  .<_  W ) 
 /\  P  =/=  Q ) )  ->  C  e.  B )
 
Theoremcdleme27a 29835* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 29831 with s and t swapped (this case is not mentioned by them). If s  <_ t  \/ v, then f(s)  <_ fs(t)  \/ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  =/=  Q  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( s  =/=  t  /\  s  .<_  ( t  .\/  V )
 )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  C  .<_  ( Y  .\/  V ) )
 
Theoremcdleme27b 29836* Lemma for cdleme27N 29837. (Contributed by NM, 3-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( s  =  t  ->  C  =  Y )
 
Theoremcdleme27N 29837* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme27a 29835. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  =/=  Q  /\  ( s  e.  A  /\  -.  s  .<_  W ) )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) 
 /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( s  .<_  ( t 
 .\/  V )  /\  ( V  e.  A  /\  V  .<_  W ) ) )  ->  C  .<_  ( Y  .\/  V )
 )
 
Theoremcdleme28a 29838* Lemma for cdleme25b 29822. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   &    |-  V  =  ( (
 s  .\/  t )  ./\  ( X  ./\  W ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  (
 s  e.  A  /\  -.  s  .<_  W )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( s  =/=  t  /\  (
 ( s  .\/  ( X  ./\  W ) )  =  X  /\  (
 t  .\/  ( X  ./\ 
 W ) )  =  X )  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) )  ->  ( C  .\/  ( X  ./\  W ) )  .<_  ( Y  .\/  ( X  ./\  W ) ) )
 
Theoremcdleme28b 29839* Lemma for cdleme25b 29822. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  (
 s  e.  A  /\  -.  s  .<_  W )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( s  =/=  t  /\  (
 ( s  .\/  ( X  ./\  W ) )  =  X  /\  (
 t  .\/  ( X  ./\ 
 W ) )  =  X )  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) )  ->  ( C  .\/  ( X  ./\  W ) )  =  ( Y 
 .\/  ( X  ./\  W ) ) )
 
Theoremcdleme28c 29840* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the  s  =/=  t antecedent in cdleme28b 29839. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  (
 s  e.  A  /\  -.  s  .<_  W )  /\  ( t  e.  A  /\  -.  t  .<_  W ) )  /\  ( ( s  .\/  ( X  ./\ 
 W ) )  =  X  /\  ( t 
 .\/  ( X  ./\  W ) )  =  X  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) )  ->  ( C  .\/  ( X  ./\  W ) )  =  ( Y  .\/  ( X  ./\ 
 W ) ) )
 
Theoremcdleme28 29841* Quantified version of cdleme28c 29840. (Compare cdleme24 29820.) (Contributed by NM, 7-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  G  =  ( (
 t  .\/  U )  ./\  ( Q  .\/  (
 ( P  .\/  t
 )  ./\  W ) ) )   &    |-  O  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( t  .\/  z )  ./\  W ) ) )   &    |-  E  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  O ) )   &    |-  Y  =  if ( t  .<_  ( P  .\/  Q ) ,  E ,  G )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  A. s  e.  A  A. t  e.  A  ( ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  /\  ( -.  t  .<_  W  /\  ( t 
 .\/  ( X  ./\  W ) )  =  X ) )  ->  ( C 
 .\/  ( X  ./\  W ) )  =  ( Y  .\/  ( X  ./\ 
 W ) ) ) )
 
Theoremcdleme29ex 29842* Lemma for cdleme29b 29843. (Compare cdleme25a 29821.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  E. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  /\  ( C  .\/  ( X  ./\  W ) )  e.  B ) )
 
Theoremcdleme29b 29843* Transform cdleme28 29841. (Compare cdleme25b 29822.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  E. v  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) 
 ->  v  =  ( C  .\/  ( X  ./\  W ) ) ) )
 
Theoremcdleme29c 29844* Transform cdleme28b 29839. (Compare cdleme25c 29823.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  E! v  e.  B  A. s  e.  A  ( ( -.  s  .<_  W 
 /\  ( s  .\/  ( X  ./\  W ) )  =  X ) 
 ->  v  =  ( C  .\/  ( X  ./\  W ) ) ) )
 
Theoremcdleme29cl 29845* Show closure of the unique element in cdleme28c 29840. (Contributed by NM, 8-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  F  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  Z  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W ) ) )   &    |-  N  =  ( ( P  .\/  Q )  ./\  ( Z  .\/  ( ( s  .\/  z )  ./\  W ) ) )   &    |-  D  =  (
 iota_ u  e.  B A. z  e.  A  ( ( -.  z  .<_  W  /\  -.  z  .<_  ( P  .\/  Q ) )  ->  u  =  N ) )   &    |-  C  =  if ( s  .<_  ( P  .\/  Q ) ,  D ,  F )   &    |-  I  =  ( iota_ v  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( X  ./\ 
 W ) )  =  X )  ->  v  =  ( C  .\/  ( X  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 ->  I  e.  B )
 
Theoremcdleme30a 29846 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( K  e.  HL  /\  W  e.  H )  /\  ( s  e.  A  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  Y  e.  B )  /\  ( ( s  .\/  ( X  ./\  W ) )  =  X  /\  X  .<_  Y ) ) 
 ->  ( s  .\/  ( Y  ./\  W ) )  =  Y )
 
Theoremcdleme31so 29847* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( x  ./\  W ) )  =  x )  ->  z  =  ( N  .\/  ( x 
 ./\  W ) ) ) )   &    |-  C  =  (
 iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  ->  z  =  ( N  .\/  ( X  ./\ 
 W ) ) ) )   =>    |-  ( X  e.  B  -> 
 [_ X  /  x ]_ O  =  C )
 
Theoremcdleme31sn 29848* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  C  =  if ( R  .<_  ( P  .\/  Q ) ,  [_ R  /  s ]_ I ,  [_ R  /  s ]_ D )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31sn1 29849* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  I  =  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  C  =  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  [_ R  /  s ]_ G ) )   =>    |-  ( ( R  e.  A  /\  R  .<_  ( P  .\/  Q ) )  ->  [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31se 29850* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  T )  ./\  W )
 ) )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  T )  ./\  W )
 ) )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ E  =  Y )
 
Theoremcdleme31se2 29851* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.)
 |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( R  .\/  t )  ./\  W ) ) )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( [_ S  /  t ]_ D  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( S  e.  A  -> 
 [_ S  /  t ]_ E  =  Y )
 
Theoremcdleme31sc 29852* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
 |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  X  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( R  e.  A  -> 
 [_ R  /  s ]_ C  =  X )
 
Theoremcdleme31sde 29853* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
 |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  E  =  ( ( P  .\/  Q )  ./\  ( D  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  Y  =  ( ( S  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  S )  ./\  W )
 ) )   &    |-  Z  =  ( ( P  .\/  Q )  ./\  ( Y  .\/  ( ( R  .\/  S )  ./\  W )
 ) )   =>    |-  ( ( R  e.  A  /\  S  e.  A )  ->  [_ R  /  s ]_ [_ S  /  t ]_ E  =  Z )
 
Theoremcdleme31snd 29854* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.)
 |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  ( ( v  .\/  V )  ./\  ( P  .\/  ( ( Q  .\/  v )  ./\  W ) ) )   &    |-  E  =  ( ( O  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  O )  ./\  W )
 ) )   &    |-  O  =  ( ( S  .\/  V )  ./\  ( P  .\/  ( ( Q  .\/  S )  ./\  W )
 ) )   =>    |-  ( S  e.  A  -> 
 [_ S  /  v ]_ [_ N  /  t ]_ D  =  E )
 
Theoremcdleme31sdnN 29855* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.)
 |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  D  =  ( ( t  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  t )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  N  =  if (
 s  .<_  ( P  .\/  Q ) ,  I ,  [_ s  /  t ]_ D )
 
Theoremcdleme31sn1c 29856* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.)
 |-  G  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( s  .\/  t )  ./\  W ) ) )   &    |-  I  =  (
 iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  G ) )   &    |-  N  =  if ( s  .<_  ( P  .\/  Q ) ,  I ,  D )   &    |-  Y  =  ( ( P  .\/  Q )  ./\  ( E  .\/  ( ( R  .\/  t )  ./\ 
 W ) ) )   &    |-  C  =  ( iota_ y  e.  B A. t  e.  A  ( ( -.  t  .<_  W  /\  -.  t  .<_  ( P  .\/  Q ) )  ->  y  =  Y ) )   =>    |-  ( ( R  e.  A  /\  R  .<_  ( P  .\/  Q ) )  ->  [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31sn2 29857* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)
 |-  D  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  D )   &    |-  C  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
 ) )   =>    |-  ( ( R  e.  A  /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  [_ R  /  s ]_ N  =  C )
 
Theoremcdleme31fv 29858* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( x  ./\  W ) )  =  x )  ->  z  =  ( N  .\/  ( x 
 ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  C  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  ->  z  =  ( N  .\/  ( X  ./\ 
 W ) ) ) )   =>    |-  ( X  e.  B  ->  ( F `  X )  =  if (
 ( P  =/=  Q  /\  -.  X  .<_  W ) ,  C ,  X ) )
 
Theoremcdleme31fv1 29859* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( x  ./\  W ) )  =  x )  ->  z  =  ( N  .\/  ( x 
 ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   &    |-  C  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  ->  z  =  ( N  .\/  ( X  ./\ 
 W ) ) ) )   =>    |-  ( ( X  e.  B  /\  ( P  =/=  Q 
 /\  -.  X  .<_  W ) )  ->  ( F `  X )  =  C )
 
Theoremcdleme31fv1s 29860* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)
 |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( x  ./\  W ) )  =  x )  ->  z  =  ( N  .\/  ( x 
 ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( X  e.  B  /\  ( P  =/=  Q  /\  -.  X  .<_  W ) ) 
 ->  ( F `  X )  =  [_ X  /  x ]_ O )
 
Theoremcdleme31fv2 29861* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.)
 |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( X  e.  B  /\  -.  ( P  =/=  Q  /\  -.  X  .<_  W ) ) 
 ->  ( F `  X )  =  X )
 
Theoremcdleme31id 29862* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.)
 |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( X  e.  B  /\  P  =  Q )  ->  ( F `  X )  =  X )
 
Theoremcdlemefrs29pre00 29863 ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 29498. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( R  e.  A  /\  -.  R  .<_  W )  /\  ps )  /\  s  e.  A )  ->  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R ) 
 <->  ( -.  s  .<_  W 
 /\  ( s  .\/  ( R  ./\  W ) )  =  R ) ) )
 
Theoremcdlemefrs29bpre0 29864* TODO fix comment. (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  ( A. s  e.  A  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s  .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\  W ) ) )  <->  z  =  [_ R  /  s ]_ N ) )
 
Theoremcdlemefrs29bpre1 29865* TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  E. z  e.  B  A. s  e.  A  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\ 
 W ) ) ) )
 
Theoremcdlemefrs29cpre1 29866* TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  E! z  e.  B  A. s  e.  A  ( ( ( -.  s  .<_  W  /\  ph )  /\  ( s 
 .\/  ( R  ./\  W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\ 
 W ) ) ) )
 
Theoremcdlemefrs29clN 29867* TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 29866. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( R  ./\ 
 W ) )  =  R )  ->  z  =  ( N  .\/  ( R  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  O  e.  B )
 
Theoremcdlemefrs32fva 29868* Part of proof of Lemma E in [Crawley] p. 113. Value of  F at an atom not under  W. TODO: FIX COMMENT TODO: consolidate uses of lhpmat 29498 here and elsewhere, and presence/absence of  s 
.<_  ( P  .\/  Q
) term. Also, why can proof be shortened with cdleme29cl 29845? What is difference from cdlemefs27cl 29881? (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  ps )  ->  [_ R  /  x ]_ O  =  [_ R  /  s ]_ N )
 
Theoremcdlemefrs32fva1 29869* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  (
 s  =  R  ->  (
 ph 
 <->  ps ) )   &    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  P  =/=  Q 
 /\  ( s  e.  A  /\  ( -.  s  .<_  W  /\  ph )
 ) )  ->  N  e.  B )   &    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  [_ R  /  s ]_ N  e.  B )   &    |-  O  =  ( iota_ z  e.  B A. s  e.  A  ( ( -.  s  .<_  W  /\  (
 s  .\/  ( x  ./\ 
 W ) )  =  x )  ->  z  =  ( N  .\/  ( x  ./\  W ) ) ) )   &    |-  F  =  ( x  e.  B  |->  if ( ( P  =/=  Q 
 /\  -.  x  .<_  W ) ,  O ,  x ) )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H ) 
 /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) 
 /\  ( P  =/=  Q 
 /\  ( R  e.  A  /\  -.  R  .<_  W ) )  /\  ps )  ->  ( F `  R )  =  [_ R  /  s ]_ N )
 
Theoremcdlemefr29exN 29870* Lemma for cdlemefs29bpre1N 29885. (Compare cdleme25a 29821.) TODO: FIX COMMENT TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   =>    |-  (
 ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( X  e.  B  /\  -.  X  .<_  W ) ) 
 /\  A. s  e.  A  C  e.  B )  ->  E. s  e.  A  ( ( -.  s  .<_  W  /\  ( s 
 .\/  ( X  ./\  W ) )  =  X )  /\  ( C  .\/  ( X  ./\  W ) )  e.  B ) )
 
Theoremcdlemefr27cl 29871 Part of proof of Lemma E in [Crawley] p. 113. Closure of  N. (Contributed by NM, 23-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  P  e.  A  /\  Q  e.  A )  /\  ( s  e.  A  /\  -.  s  .<_  ( P 
 .\/  Q )  /\  P  =/=  Q ) )  ->  N  e.  B )
 
Theoremcdlemefr32sn2aw 29872* Show that  [_ R  / 
s ]_ N is an atom not under  W when  -.  R  .<_  ( P  .\/  Q ). (Contributed by NM, 28-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  ( [_ R  /  s ]_ N  e.  A  /\  -.  [_ R  /  s ]_ N  .<_  W ) )
 
Theoremcdlemefr32snb 29873* Show closure of  [_ R  /  s ]_ N. (Contributed by NM, 28-Mar-2013.)
 |-  B  =  ( Base `  K )   &    |-  .<_  =  ( le `  K )   &    |- 
 .\/  =  ( join `  K )   &    |-  ./\  =  ( meet `  K )   &    |-  A  =  ( Atoms `  K )   &    |-  H  =  ( LHyp `  K )   &    |-  U  =  ( ( P  .\/  Q )  ./\  W )   &    |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W ) ) )   &    |-  N  =  if ( s  .<_  ( P 
 .\/  Q ) ,  I ,  C )   =>    |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) 
 /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  /\  ( P  =/=  Q  /\  ( R  e.  A  /\  -.  R  .<_  W ) ) 
 /\  -.  R  .<_  ( P  .\/  Q )
 )  ->  [_ R  /  s ]_ N  e.  B )
 
Theorem<