pltle - Metamath Proof Explorer

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

Theorem pltle 18412

Description: "Less than" implies "less than or equal to". (pssss 4055 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 18411	. . 3 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
4	3	simprbda 504	. 2 ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 < 𝑌) → 𝑋 ≤ 𝑌)
5	4	ex 418	1 ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 class class class wbr 5114 ‘cfv 6543 lecple 17342 ltcplt 18389

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pr 5409

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-iota 6499 df-fun 6545 df-fv 6551 df-plt 18409

This theorem is used by: pleval2 18416 pltnlt 18419 pltn2lp 18420 plttr 18421 pospo 18424 ogrpaddlt 20239 orngsqr 21006 ornglmullt 21009 orngrmullt 21010 isarchi3 33538 archirngz 33540 archiabllem2a 33545 atnlt 40128 cvlcvr1 40154 hlrelat 40217 hlrelat3 40227 cvratlem 40236 atltcvr 40250 atlelt 40253 llnnlt 40338 lplnnle2at 40356 lplnnlt 40380 lvolnle3at 40397 lvolnltN 40433 cdlemblem 40608 cdlemb 40609 lhpexle1 40823

W3C validator