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

Theorem pltval 17275
Description: Less-than relation. (df-pss 3785 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 17274 . . . 4 (𝐾𝐴< = ( ∖ I ))
43breqd 4854 . . 3 (𝐾𝐴 → (𝑋 < 𝑌𝑋( ∖ I )𝑌))
5 brdif 4896 . . . 4 (𝑋( ∖ I )𝑌 ↔ (𝑋 𝑌 ∧ ¬ 𝑋 I 𝑌))
6 ideqg 5477 . . . . . . 7 (𝑌𝐶 → (𝑋 I 𝑌𝑋 = 𝑌))
76necon3bbid 3008 . . . . . 6 (𝑌𝐶 → (¬ 𝑋 I 𝑌𝑋𝑌))
87adantl 474 . . . . 5 ((𝑋𝐵𝑌𝐶) → (¬ 𝑋 I 𝑌𝑋𝑌))
98anbi2d 623 . . . 4 ((𝑋𝐵𝑌𝐶) → ((𝑋 𝑌 ∧ ¬ 𝑋 I 𝑌) ↔ (𝑋 𝑌𝑋𝑌)))
105, 9syl5bb 275 . . 3 ((𝑋𝐵𝑌𝐶) → (𝑋( ∖ I )𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
114, 10sylan9bb 506 . 2 ((𝐾𝐴 ∧ (𝑋𝐵𝑌𝐶)) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
12113impb 1144 1 ((𝐾𝐴𝑋𝐵𝑌𝐶) → (𝑋 < 𝑌 ↔ (𝑋 𝑌𝑋𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157  wne 2971  cdif 3766   class class class wbr 4843   I cid 5219  cfv 6101  lecple 16274  ltcplt 17256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pr 5097
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-iota 6064  df-fun 6103  df-fv 6109  df-plt 17273
This theorem is referenced by:  pltle  17276  pltne  17277  pleval2i  17279  pltnle  17281  pltval3  17282  plttr  17285  latnlemlt  17399  latnle  17400  ipolt  17474  ogrpaddlt  30234  ogrpsublt  30238  ornglmullt  30323  orngrmullt  30324  orngmullt  30325  ofldlt1  30329  opltn0  35211  cvrval2  35295  cvrnbtwn2  35296  cvrnbtwn3  35297  cvrle  35299  cvrnbtwn4  35300  cvrne  35302  atlltn0  35327  hlrelat5N  35422  llnle  35539  lplnle  35561  llncvrlpln2  35578  lplncvrlvol2  35636  lhp2lt  36022  lautlt  36112
  Copyright terms: Public domain W3C validator