Metamath Proof Explorer


Theorem cvrnle

Description: The covers relation implies the negation of the converse "less than or equal to" relation. (Contributed by NM, 18-Oct-2011)

Ref Expression
Hypotheses cvrle.b 𝐵 = ( Base ‘ 𝐾 )
cvrle.l = ( le ‘ 𝐾 )
cvrle.c 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrnle ( ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ 𝑌 𝑋 )

Proof

Step Hyp Ref Expression
1 cvrle.b 𝐵 = ( Base ‘ 𝐾 )
2 cvrle.l = ( le ‘ 𝐾 )
3 cvrle.c 𝐶 = ( ⋖ ‘ 𝐾 )
4 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
5 1 4 3 cvrlt ( ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
6 1 2 4 pltnle ( ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ¬ 𝑌 𝑋 )
7 5 6 syldan ( ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ 𝑌 𝑋 )