Description: "Less than" implies "less than or equal to". ( pssss analog.) (Contributed by NM, 4-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pltval.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
pltval.s | ⊢ < = ( lt ‘ 𝐾 ) | ||
Assertion | pltle | ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pltval.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
2 | pltval.s | ⊢ < = ( lt ‘ 𝐾 ) | |
3 | 1 2 | pltval | ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
4 | 3 | simprbda | ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝑋 < 𝑌 ) → 𝑋 ≤ 𝑌 ) |
5 | 4 | ex | ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) ) |