Theorem pltle 18268

Description: "Less than" implies "less than or equal to". (pssss 4091 analog.) (Contributed by NM, 4-Dec-2011.)

Hypotheses

Ref	Expression
pltval.l	⊢ ≤ = (le‘𝐾)
pltval.s	⊢ < = (lt‘𝐾)

Assertion

Ref	Expression
pltle	⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))

Proof of Theorem pltle

Step	Hyp	Ref	Expression
1		pltval.l	. . . 4 ⊢ ≤ = (le‘𝐾)
2		pltval.s	. . . 4 ⊢ < = (lt‘𝐾)
3	1, 2	pltval 18267	. . 3 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
4	3	simprbda 499	. 2 ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 < 𝑌) → 𝑋 ≤ 𝑌)
5	4	ex 413	1 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2939   class class class wbr 5141  ‘cfv 6532  lecple 17186  ltcplt 18243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-iota 6484  df-fun 6534  df-fv 6540  df-plt 18265

This theorem is referenced by:  pleval2  18272  pltnlt  18275  pltn2lp  18276  plttr  18277  pospo  18280  ogrpaddlt  32106  isarchi3  32204  archirngz  32206  archiabllem2a  32211  orngsqr  32284  ornglmullt  32287  orngrmullt  32288  atnlt  37988  cvlcvr1  38014  hlrelat  38078  hlrelat3  38088  cvratlem  38097  atltcvr  38111  atlelt  38114  llnnlt  38199  lplnnle2at  38217  lplnnlt  38241  lvolnle3at  38258  lvolnltN  38294  cdlemblem  38469  cdlemb  38470  lhpexle1  38684