This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pltnle

Description: "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011)

Ref Expression
Hypotheses pleval2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pleval2.l ⊢ ≤ = ( le ‘ 𝐾 )
pleval2.s ⊢ < = ( lt ‘ 𝐾 )
Assertion pltnle ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ¬ 𝑌 ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 pleval2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pleval2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pleval2.s ⊢ < = ( lt ‘ 𝐾 )
4 2 3 pltval ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
5 1 2 posasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )
6 5 biimpd ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) )
7 6 expdimp ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑌 ≤ 𝑋 → 𝑋 = 𝑌 ) )
8 7 necon3ad ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ≠ 𝑌 → ¬ 𝑌 ≤ 𝑋 ) )
9 8 expimpd ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) → ¬ 𝑌 ≤ 𝑋 ) )
10 4 9 sylbid ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ¬ 𝑌 ≤ 𝑋 ) )
11 10 imp ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 < 𝑌 ) → ¬ 𝑌 ≤ 𝑋 )