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

Theorem pltval 18289
Description: Less-than relation. (df-pss 3966 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 18288 . . . 4 (𝐾 ∈ 𝐴 β†’ < = ( ≀ βˆ– I ))
43breqd 5158 . . 3 (𝐾 ∈ 𝐴 β†’ (𝑋 < π‘Œ ↔ 𝑋( ≀ βˆ– I )π‘Œ))
5 brdif 5200 . . . 4 (𝑋( ≀ βˆ– I )π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ Β¬ 𝑋 I π‘Œ))
6 ideqg 5850 . . . . . . 7 (π‘Œ ∈ 𝐢 β†’ (𝑋 I π‘Œ ↔ 𝑋 = π‘Œ))
76necon3bbid 2976 . . . . . 6 (π‘Œ ∈ 𝐢 β†’ (Β¬ 𝑋 I π‘Œ ↔ 𝑋 β‰  π‘Œ))
87adantl 480 . . . . 5 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐢) β†’ (Β¬ 𝑋 I π‘Œ ↔ 𝑋 β‰  π‘Œ))
98anbi2d 627 . . . 4 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐢) β†’ ((𝑋 ≀ π‘Œ ∧ Β¬ 𝑋 I π‘Œ) ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
105, 9bitrid 282 . . 3 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐢) β†’ (𝑋( ≀ βˆ– I )π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
114, 10sylan9bb 508 . 2 ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐢)) β†’ (𝑋 < π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
12113impb 1113 1 ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐢) β†’ (𝑋 < π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938   βˆ– cdif 3944   class class class wbr 5147   I cid 5572  β€˜cfv 6542  lecple 17208  ltcplt 18265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-plt 18287
This theorem is referenced by:  pltle  18290  pltne  18291  pleval2i  18293  pltnle  18295  pltval3  18296  plttr  18299  latnlemlt  18429  latnle  18430  ipolt  18492  ogrpaddlt  32505  ogrpsublt  32509  ornglmullt  32695  orngrmullt  32696  orngmullt  32697  ofldlt1  32701  opltn0  38363  cvrval2  38447  cvrnbtwn2  38448  cvrnbtwn3  38449  cvrle  38451  cvrnbtwn4  38452  cvrne  38454  atlltn0  38479  hlrelat5N  38575  llnle  38692  lplnle  38714  llncvrlpln2  38731  lplncvrlvol2  38789  lhp2lt  39175  lautlt  39265
  Copyright terms: Public domain W3C validator