MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pltle Structured version   Unicode version

Theorem pltle 15230
Description: Less-than implies less-than-or-equal. (pssss 3546 analog.) (Contributed by NM, 4-Dec-2011.)
Hypotheses
Ref Expression
pltval.l  |-  .<_  =  ( le `  K )
pltval.s  |-  .<  =  ( lt `  K )
Assertion
Ref Expression
pltle  |-  ( ( K  e.  A  /\  X  e.  B  /\  Y  e.  C )  ->  ( X  .<  Y  ->  X  .<_  Y ) )

Proof of Theorem pltle
StepHypRef Expression
1 pltval.l . . . 4  |-  .<_  =  ( le `  K )
2 pltval.s . . . 4  |-  .<  =  ( lt `  K )
31, 2pltval 15229 . . 3  |-  ( ( K  e.  A  /\  X  e.  B  /\  Y  e.  C )  ->  ( X  .<  Y  <->  ( X  .<_  Y  /\  X  =/= 
Y ) ) )
43simprbda 623 . 2  |-  ( ( ( K  e.  A  /\  X  e.  B  /\  Y  e.  C
)  /\  X  .<  Y )  ->  X  .<_  Y )
54ex 434 1  |-  ( ( K  e.  A  /\  X  e.  B  /\  Y  e.  C )  ->  ( X  .<  Y  ->  X  .<_  Y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965    = wceq 1370    e. wcel 1758    =/= wne 2642   class class class wbr 4387   ` cfv 5513   lecple 14344   ltcplt 15210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4508  ax-nul 4516  ax-pr 4626
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3067  df-sbc 3282  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-nul 3733  df-if 3887  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4187  df-br 4388  df-opab 4446  df-mpt 4447  df-id 4731  df-xp 4941  df-rel 4942  df-cnv 4943  df-co 4944  df-dm 4945  df-iota 5476  df-fun 5515  df-fv 5521  df-plt 15227
This theorem is referenced by:  pleval2  15234  pltnlt  15237  pltn2lp  15238  plttr  15239  pospo  15242  ogrpaddlt  26312  isarchi3  26335  archirngz  26337  archiabllem2a  26342  orngsqr  26403  ornglmullt  26406  orngrmullt  26407  atnlt  33261  cvlcvr1  33287  hlrelat  33349  hlrelat3  33359  cvratlem  33368  atltcvr  33382  atlelt  33385  llnnlt  33470  lplnnle2at  33488  lplnnlt  33512  lvolnle3at  33529  lvolnltN  33565  cdlemblem  33740  cdlemb  33741  lhpexle1  33955
  Copyright terms: Public domain W3C validator