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

Theorem pltval 15244
Description: Less-than relation. (df-pss 3447 analog.) (Contributed by NM, 12-Oct-2011.)
Hypotheses
Ref Expression
pltval.l  |-  .<_  =  ( le `  K )
pltval.s  |-  .<  =  ( lt `  K )
Assertion
Ref Expression
pltval  |-  ( ( K  e.  A  /\  X  e.  B  /\  Y  e.  C )  ->  ( X  .<  Y  <->  ( X  .<_  Y  /\  X  =/= 
Y ) ) )

Proof of Theorem pltval
StepHypRef Expression
1 pltval.l . . . . 5  |-  .<_  =  ( le `  K )
2 pltval.s . . . . 5  |-  .<  =  ( lt `  K )
31, 2pltfval 15243 . . . 4  |-  ( K  e.  A  ->  .<  =  (  .<_  \  _I  )
)
43breqd 4406 . . 3  |-  ( K  e.  A  ->  ( X  .<  Y  <->  X (  .<_ 
\  _I  ) Y ) )
5 brdif 4445 . . . 4  |-  ( X (  .<_  \  _I  ) Y 
<->  ( X  .<_  Y  /\  -.  X  _I  Y
) )
6 ideqg 5094 . . . . . . 7  |-  ( Y  e.  C  ->  ( X  _I  Y  <->  X  =  Y ) )
76necon3bbid 2696 . . . . . 6  |-  ( Y  e.  C  ->  ( -.  X  _I  Y  <->  X  =/=  Y ) )
87adantl 466 . . . . 5  |-  ( ( X  e.  B  /\  Y  e.  C )  ->  ( -.  X  _I  Y 
<->  X  =/=  Y ) )
98anbi2d 703 . . . 4  |-  ( ( X  e.  B  /\  Y  e.  C )  ->  ( ( X  .<_  Y  /\  -.  X  _I  Y )  <->  ( X  .<_  Y  /\  X  =/= 
Y ) ) )
105, 9syl5bb 257 . . 3  |-  ( ( X  e.  B  /\  Y  e.  C )  ->  ( X (  .<_  \  _I  ) Y  <->  ( X  .<_  Y  /\  X  =/= 
Y ) ) )
114, 10sylan9bb 699 . 2  |-  ( ( K  e.  A  /\  ( X  e.  B  /\  Y  e.  C
) )  ->  ( X  .<  Y  <->  ( X  .<_  Y  /\  X  =/= 
Y ) ) )
12113impb 1184 1  |-  ( ( K  e.  A  /\  X  e.  B  /\  Y  e.  C )  ->  ( X  .<  Y  <->  ( X  .<_  Y  /\  X  =/= 
Y ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758    =/= wne 2645    \ cdif 3428   class class class wbr 4395    _I cid 4734   ` cfv 5521   lecple 14359   ltcplt 15225
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 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pr 4634
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 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-sbc 3289  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-iota 5484  df-fun 5523  df-fv 5529  df-plt 15242
This theorem is referenced by:  pltle  15245  pltne  15246  pleval2i  15248  pltnle  15250  pltval3  15251  plttr  15254  latnlemlt  15368  latnle  15369  ipolt  15443  ogrpaddlt  26321  ogrpsublt  26325  ornglmullt  26415  orngrmullt  26416  orngmullt  26417  ofldlt1  26421  opltn0  33154  cvrval2  33238  cvrnbtwn2  33239  cvrnbtwn3  33240  cvrle  33242  cvrnbtwn4  33243  cvrne  33245  atlltn0  33270  hlrelat5N  33364  llnle  33481  lplnle  33503  llncvrlpln2  33520  lplncvrlvol2  33578  lhp2lt  33964  lautlt  34054
  Copyright terms: Public domain W3C validator