Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dalemkelat Unicode version

Theorem dalemkelat 29813
Description: Lemma for dath 29925. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.)
Hypothesis
Ref Expression
dalema.ph  |-  ( ph  <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A
) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  ( ( -.  C  .<_  ( P  .\/  Q
)  /\  -.  C  .<_  ( Q  .\/  R
)  /\  -.  C  .<_  ( R  .\/  P
) )  /\  ( -.  C  .<_  ( S 
.\/  T )  /\  -.  C  .<_  ( T 
.\/  U )  /\  -.  C  .<_  ( U 
.\/  S ) )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
.\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )
Assertion
Ref Expression
dalemkelat  |-  ( ph  ->  K  e.  Lat )

Proof of Theorem dalemkelat
StepHypRef Expression
1 dalema.ph . . 3  |-  ( ph  <->  ( ( ( K  e.  HL  /\  C  e.  ( Base `  K
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  R  e.  A )  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A
) )  /\  ( Y  e.  O  /\  Z  e.  O )  /\  ( ( -.  C  .<_  ( P  .\/  Q
)  /\  -.  C  .<_  ( Q  .\/  R
)  /\  -.  C  .<_  ( R  .\/  P
) )  /\  ( -.  C  .<_  ( S 
.\/  T )  /\  -.  C  .<_  ( T 
.\/  U )  /\  -.  C  .<_  ( U 
.\/  S ) )  /\  ( C  .<_  ( P  .\/  S )  /\  C  .<_  ( Q 
.\/  T )  /\  C  .<_  ( R  .\/  U ) ) ) ) )
21dalemkehl 29812 . 2  |-  ( ph  ->  K  e.  HL )
3 hllat 29553 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
42, 3syl 15 1  |-  ( ph  ->  K  e.  Lat )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    e. wcel 1684   class class class wbr 4023   ` cfv 5255  (class class class)co 5858   Basecbs 13148   Latclat 14151   HLchlt 29540
This theorem is referenced by:  dalemcnes  29839  dalempnes  29840  dalemqnet  29841  dalemply  29843  dalemsly  29844  dalem1  29848  dalemcea  29849  dalem3  29853  dalem4  29854  dalem5  29856  dalem8  29859  dalem-cly  29860  dalem10  29862  dalem13  29865  dalem16  29868  dalem17  29869  dalem21  29883  dalem25  29887  dalem27  29888  dalem38  29899  dalem39  29900  dalem43  29904  dalem44  29905  dalem45  29906  dalem48  29909  dalem54  29915  dalem55  29916  dalem56  29917  dalem57  29918  dalem60  29921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-atl 29488  df-cvlat 29512  df-hlat 29541
  Copyright terms: Public domain W3C validator