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

Theorem pltval 16954
Description: Less-than relation. (df-pss 3588 analog.) (Contributed by NM, 12-Oct-2011.)
Hypotheses
Ref Expression
pltval.l = (le‘𝐾)
pltval.s < = (lt‘𝐾)
Assertion
Ref Expression
pltval ((𝐾𝐴𝑋𝐵𝑌𝐶) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))

Proof of Theorem pltval
StepHypRef Expression
1 pltval.l . . . . 5 = (le‘𝐾)
2 pltval.s . . . . 5 < = (lt‘𝐾)
31, 2pltfval 16953 . . . 4 (𝐾𝐴< = ( ∖ I ))
43breqd 4662 . . 3 (𝐾𝐴 → (𝑋 < 𝑌𝑋( ∖ I )𝑌))
5 brdif 4703 . . . 4 (𝑋( ∖ I )𝑌 ↔ (𝑋 𝑌 ∧ ¬ 𝑋 I 𝑌))
6 ideqg 5271 . . . . . . 7 (𝑌𝐶 → (𝑋 I 𝑌𝑋 = 𝑌))
76necon3bbid 2830 . . . . . 6 (𝑌𝐶 → (¬ 𝑋 I 𝑌𝑋𝑌))
87adantl 482 . . . . 5 ((𝑋𝐵𝑌𝐶) → (¬ 𝑋 I 𝑌𝑋𝑌))
98anbi2d 740 . . . 4 ((𝑋𝐵𝑌𝐶) → ((𝑋 𝑌 ∧ ¬ 𝑋 I 𝑌) ↔ (𝑋 𝑌𝑋𝑌)))
105, 9syl5bb 272 . . 3 ((𝑋𝐵𝑌𝐶) → (𝑋( ∖ I )𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
114, 10sylan9bb 736 . 2 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐶)) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
12113impb 1259 1 ((𝐾𝐴𝑋𝐵𝑌𝐶) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wcel 1989  wne 2793  cdif 3569   class class class wbr 4651   I cid 5021  cfv 5886  lecple 15942  ltcplt 16935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-mpt 4728  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-iota 5849  df-fun 5888  df-fv 5894  df-plt 16952
This theorem is referenced by:  pltle  16955  pltne  16956  pleval2i  16958  pltnle  16960  pltval3  16961  plttr  16964  latnlemlt  17078  latnle  17079  ipolt  17153  ogrpaddlt  29703  ogrpsublt  29707  ornglmullt  29792  orngrmullt  29793  orngmullt  29794  ofldlt1  29798  opltn0  34303  cvrval2  34387  cvrnbtwn2  34388  cvrnbtwn3  34389  cvrle  34391  cvrnbtwn4  34392  cvrne  34394  atlltn0  34419  hlrelat5N  34513  llnle  34630  lplnle  34652  llncvrlpln2  34669  lplncvrlvol2  34727  lhp2lt  35113  lautlt  35203
  Copyright terms: Public domain W3C validator