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

Theorem pltval 17182
Description: Less-than relation. (df-pss 3732 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 17181 . . . 4 (𝐾𝐴< = ( ∖ I ))
43breqd 4816 . . 3 (𝐾𝐴 → (𝑋 < 𝑌𝑋( ∖ I )𝑌))
5 brdif 4858 . . . 4 (𝑋( ∖ I )𝑌 ↔ (𝑋 𝑌 ∧ ¬ 𝑋 I 𝑌))
6 ideqg 5430 . . . . . . 7 (𝑌𝐶 → (𝑋 I 𝑌𝑋 = 𝑌))
76necon3bbid 2970 . . . . . 6 (𝑌𝐶 → (¬ 𝑋 I 𝑌𝑋𝑌))
87adantl 473 . . . . 5 ((𝑋𝐵𝑌𝐶) → (¬ 𝑋 I 𝑌𝑋𝑌))
98anbi2d 742 . . . 4 ((𝑋𝐵𝑌𝐶) → ((𝑋 𝑌 ∧ ¬ 𝑋 I 𝑌) ↔ (𝑋 𝑌𝑋𝑌)))
105, 9syl5bb 272 . . 3 ((𝑋𝐵𝑌𝐶) → (𝑋( ∖ I )𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
114, 10sylan9bb 738 . 2 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐶)) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
12113impb 1108 1 ((𝐾𝐴𝑋𝐵𝑌𝐶) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2140  wne 2933  cdif 3713   class class class wbr 4805   I cid 5174  cfv 6050  lecple 16171  ltcplt 17163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-iota 6013  df-fun 6052  df-fv 6058  df-plt 17180
This theorem is referenced by:  pltle  17183  pltne  17184  pleval2i  17186  pltnle  17188  pltval3  17189  plttr  17192  latnlemlt  17306  latnle  17307  ipolt  17381  ogrpaddlt  30049  ogrpsublt  30053  ornglmullt  30138  orngrmullt  30139  orngmullt  30140  ofldlt1  30144  opltn0  34999  cvrval2  35083  cvrnbtwn2  35084  cvrnbtwn3  35085  cvrle  35087  cvrnbtwn4  35088  cvrne  35090  atlltn0  35115  hlrelat5N  35209  llnle  35326  lplnle  35348  llncvrlpln2  35365  lplncvrlvol2  35423  lhp2lt  35809  lautlt  35899
  Copyright terms: Public domain W3C validator